IsAddHom.neg
theorem IsAddHom.neg :
∀ {α : Type u_2} {β : Type u_3} [inst : Add α] [inst_1 : AddCommGroup β] {f : α → β},
IsAddHom f → IsAddHom fun a => -f a
This theorem states that if you have a function `f` from type `α` to type `β`, where `α` has an addition operation and `β` is a commutative group with an addition operation, and if this function `f` preserves addition (i.e., is an "addition homomorphism"), then the negation of `f` (a function that maps each element of `α` to the negation of its image under `f`) also preserves addition. In other words, the negative of an addition-preserving function is also addition-preserving when the function's target is a commutative group.
More concisely: If `f: α -> β` preserves addition with `α` being an abelian group and `β` being a commutative group, then the negation of `f` also preserves addition.
|
IsMulHom.inv
theorem IsMulHom.inv :
∀ {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : CommGroup β] {f : α → β},
IsMulHom f → IsMulHom fun a => (f a)⁻¹
This theorem states that if a function `f` from a type `α` to a type `β` preserves multiplication (i.e., is a multiplication homomorphism), then the inverse of `f`, which maps each element of `α` to the inverse of its image under `f`, also preserves multiplication, provided that multiplication on `β` is commutative. This theorem holds for any types `α` and `β` such that `α` has a multiplication operation and `β` is a commutative group under multiplication.
More concisely: If `f : α → β` preserves multiplication and `β` is a commutative group under multiplication, then the inverse of `f` also preserves multiplication.
|
IsAddMonoidHom.map_zero
theorem IsAddMonoidHom.map_zero :
∀ {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst_1 : AddZeroClass β] {f : α → β},
IsAddMonoidHom f → f 0 = 0
This theorem states that if a function `f` is an additive monoid homomorphism mapping from type `α` to type `β`, both of which are additive zero classes, then `f` preserves the additive identity. In other words, if you apply the function `f` to the additive identity (zero) of `α`, then the result will be the additive identity (zero) of `β`.
More concisely: If `f` is an additive monoid homomorphism from additive zero class `α` to additive zero class `β`, then `f 0 = 0`, where `0` denotes the additive identities of `α` and `β` respectively.
|
IsAddHom.comp
theorem IsAddHom.comp :
∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] {γ : Type u_1} [inst_2 : Add γ] {f : α → β} {g : β → γ},
IsAddHom f → IsAddHom g → IsAddHom (g ∘ f)
This theorem states that if you have two functions, `f` and `g`, where `f` maps from some type `α` to type `β`, and `g` maps from type `β` to type `γ`, if both `f` and `g` preserve the operation of addition (they are additive homomorphisms), then the composition of `g` and `f` (i.e., `g ∘ f`) also preserves addition. This result holds in any context where `α`, `β`, and `γ` are types equipped with an addition operation.
More concisely: If `f: α → β` and `g: β → γ` are additive homomorphisms, then their composition `g ∘ f` is also an additive homomorphism.
|
IsAddMonoidHom.comp
theorem IsAddMonoidHom.comp :
∀ {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst_1 : AddZeroClass β] {f : α → β},
IsAddMonoidHom f →
∀ {γ : Type u_1} [inst_2 : AddZeroClass γ] {g : β → γ}, IsAddMonoidHom g → IsAddMonoidHom (g ∘ f)
This theorem states that if you have two additive monoid homomorphisms, one from a type `α` to a type `β` and the other from `β` to another type `γ` (where `α`, `β`, and `γ` are types with an addition operation and a zero element), then the composition of these two homomorphisms (first applying `f`, then applying `g`) is itself an additive monoid homomorphism. In other words, the property of being a homomorphism is preserved when you compose two homomorphisms.
More concisely: If `f : α -> β` and `g : β -> γ` are additive monoid homomorphisms, then their composition `g ∘ f : α -> γ` is also an additive monoid homomorphism.
|
IsGroupHom.id
theorem IsGroupHom.id : ∀ {α : Type u} [inst : Group α], IsGroupHom id
This theorem states that the identity function is a group homomorphism for any given group. In other words, if you have a group (a mathematical structure with a set of elements, a binary operation, an identity element, and an inverse operation), the function that maps each element to itself (the identity function) will preserve the group structure, meaning that it will maintain the properties of the group's operations when mapping from the group to itself.
More concisely: The identity function is a group homomorphism for any group. In other words, for all groups G and all elements a, b in G, the equation holding in G (a * b) = c implies the equality a = b => a = c under function application to the identity function. (Here, "*" denotes the group operation and "=" denotes equality.)
|
IsGroupHom.mk'
theorem IsGroupHom.mk' :
∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Group β] {f : α → β},
(∀ (x y : α), f (x * y) = f x * f y) → IsGroupHom f
This theorem, `IsGroupHom.mk'`, allows you to construct an instance of `IsGroupHom`, which represents a group homomorphism, given the only required hypothesis. Specifically, for any types `α` and `β` that are groups, and any function `f` from `α` to `β`, if it holds that for all `x` and `y` in `α`, the image of the product `x * y` under `f` equals the product of the images `f(x)` and `f(y)`, then `f` is a group homomorphism.
More concisely: If `f` is a function between groups `α` and `β` such that `f(x * y) = f(x) * f(y)` for all `x, y` in `α`, then `f` is a group homomorphism.
|
IsGroupHom.to_isMonoidHom
theorem IsGroupHom.to_isMonoidHom :
∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Group β] {f : α → β}, IsGroupHom f → IsMonoidHom f := by
sorry
This theorem states that a group homomorphism is also a monoid homomorphism. Given two types, `α` and `β`, and assuming that both types form groups (as indicated by the instances `Group α` and `Group β`), if a function `f` from `α` to `β` is a group homomorphism (`IsGroupHom f`), then this theorem asserts that `f` is also a monoid homomorphism (`IsMonoidHom f`). This is a general result in abstract algebra, reflecting the fact that a group is a special kind of monoid, hence any properties (like being a homomorphism) that hold for groups also hold for monoids.
More concisely: If `f` is a group homomorphism between groups `α` and `β`, then `f` is also a monoid homomorphism between the underlying monoids of `α` and `β`.
|
IsAddGroupHom.sub
theorem IsAddGroupHom.sub :
∀ {α : Type u_1} {β : Type u_2} [inst : AddGroup α] [inst_1 : AddCommGroup β] {f g : α → β},
IsAddGroupHom f → IsAddGroupHom g → IsAddGroupHom fun a => f a - g a
This theorem states that if you have two functions, `f` and `g`, from an additive group `α` to a commutative additive group `β`, and both `f` and `g` are additive group homomorphisms (i.e., they preserve the group operation), then the function that takes an element `a` from `α` and maps it to the difference `f(a) - g(a)` in `β` is also an additive group homomorphism.
More concisely: If `f` and `g` are additive group homomorphisms from an additive group `α` to a commutative additive group `β`, then the function `a ↔> f(a) - g(a)` is an additive group homomorphism from `α` to `β`.
|
IsAddGroupHom.neg
theorem IsAddGroupHom.neg :
∀ {α : Type u_1} {β : Type u_2} [inst : AddGroup α] [inst_1 : AddCommGroup β] {f : α → β},
IsAddGroupHom f → IsAddGroupHom fun a => -f a
This theorem states that the negation of an additive group homomorphism is itself an additive group homomorphism, given that the target group is commutative. In other words, for any types α and β, where α is an additive group and β is a commutative additive group, if a function 'f' from α to β is an additive group homomorphism, then the function that maps each element of α to the additive inverse of its image under 'f' is also an additive group homomorphism.
More concisely: If 'f': α → β is an additive group homomorphism from an additive group α to a commutative additive group β, then the function that maps each x in α to the additive inverse of f(x) is also an additive group homomorphism.
|
IsMulHom.to_isMonoidHom
theorem IsMulHom.to_isMonoidHom :
∀ {α : Type u} {β : Type v} [inst : MulOneClass α] [inst_1 : Group β] {f : α → β}, IsMulHom f → IsMonoidHom f := by
sorry
This theorem states that for any two types 'α' and 'β', given 'α' is a multiplicative monoid (a structure with multiplication operation and a multiplicative identity), 'β' is a group (a structure with multiplication, inverse, and identity operations), and 'f' is a function from 'α' to 'β', if the function 'f' preserves the multiplication operation (i.e., is a multiplication-preserving map or "mul-hom"), then 'f' is also a monoid homomorphism. A monoid homomorphism is a function that preserves the operations of a monoid, namely the multiplication operation and the identity element.
More concisely: Given 'α' is a multiplicative monoid, 'β' is a group, and 'f' is a multiplication-preserving map from 'α' to 'β', then 'f' is a monoid homomorphism.
|
IsAddGroupHom.id
theorem IsAddGroupHom.id : ∀ {α : Type u} [inst : AddGroup α], IsAddGroupHom id
This theorem states that the identity function is an additive group homomorphism for any type `α` that forms an additive group. In mathematics, an additive group is a set equipped with an addition operation that satisfies certain properties, and a group homomorphism is a function between two groups that preserves the group structure. Here, the identity function, which maps any element to itself, is shown to preserve the structure of an additive group.
More concisely: The identity function is a homomorphism for any additive group.
|
IsAddGroupHom.mk'
theorem IsAddGroupHom.mk' :
∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddGroup β] {f : α → β},
(∀ (x y : α), f (x + y) = f x + f y) → IsAddGroupHom f
This theorem allows us to construct an `IsAddGroupHom` instance given its only defining property. In more detail, for all types `α` and `β` that have `AddGroup` structures, and for any function `f` from `α` to `β`, if `f` preserves the addition operation (i.e., for all `x` and `y` in `α`, `f` of `x + y` equals `f x + f y`), then `f` is an additive group homomorphism.
More concisely: If `α` and `β` are AddGroups and a function `f: α → β` satisfies `f (x + y) = f x + f y` for all `x, y ∈ α`, then `f` is an additive group homomorphism.
|
IsMulHom.id
theorem IsMulHom.id : ∀ {α : Type u} [inst : Mul α], IsMulHom id
This theorem states that the identity map preserves the operation of multiplication for any type `α` with a multiplication operation. In other words, if we have an arbitrary type `α` that is part of a multiplication group, the identity map will not change the product of two elements from this type. This is a specific instance of the broader mathematical concept that identity operations preserve the structure of algebraic operations.
More concisely: For any type `α` with a multiplication operation, the identity map preserves the multiplication, that is, for all `a, b : α`, `id α a * id α b = a * b`.
|
AddEquiv.isAddMonoidHom
theorem AddEquiv.isAddMonoidHom :
∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (h : M ≃+ N), IsAddMonoidHom ⇑h
This theorem states that for any two types `M` and `N`, which have the structure of additive monoids (meaning that they have an operation of addition and a zero element), any additive bijection `h` between them is also an additive monoid homomorphism. In mathematical terms, if `M` and `N` are additive monoids, then any bijective map `h : M -> N` that preserves the addition operation and the zero element is a homomorphism of additive monoids. Note that this theorem is deprecated, suggesting that there's a more recent or preferred way to express this concept in Lean 4.
More concisely: If `h : M -> N` is a bijective additive monoid homomorphism between additive monoids `M` and `N`, then `h` preserves addition and zero elements: `h(x + y) = h(x) + h(y)` and `h(0) = 0`.
|
IsAddMonoidHom.neg
theorem IsAddMonoidHom.neg :
∀ {α : Type u_1} {β : Type u_2} [inst : AddZeroClass α] [inst_1 : AddCommGroup β] {f : α → β},
IsAddMonoidHom f → IsAddMonoidHom fun a => -f a
This theorem asserts that the negation of a function that preserves addition, also preserves addition under the condition that the target set forms a commutative group under addition. More specifically, for any types `α` and `β`, where `α` is an additive monoid (a set equipped with an associative addition operation and a zero element) and `β` is an additive commutative group (an additive monoid where every element has an additive inverse), if a function `f` from `α` to `β` is an additive monoid homomorphism (it preserves the addition operation and maps the zero element of `α` to the zero element of `β`), then the function that maps each element of `α` to the additive inverse of its image under `f` is also an additive monoid homomorphism. This is stated formally in Lean 4 as `IsAddMonoidHom f → IsAddMonoidHom fun a => -f a`.
More concisely: If `f` is an additive homomorphism from an additive monoid `α` to an additive commutative group `β`, then the function mapping each element `a` in `α` to the additive inverse of `f(a)` in `β` is also an additive homomorphism.
|
IsAddHom.map_add
theorem IsAddHom.map_add :
∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Add β] {f : α → β},
IsAddHom f → ∀ (x y : α), f (x + y) = f x + f y
This theorem, `IsAddHom.map_add`, states that for any function `f` that maps from one additive type `α` to another additive type `β`, if `f` is an additive homomorphism (as denoted by `IsAddHom f`), then `f` preserves the operation of addition. In terms of mathematics, this means that for any two elements `x` and `y` in `α`, the value of `f` applied to the sum of `x` and `y` (i.e., `f (x + y)`) is equal to the sum of the values of `f` applied to `x` and `y` separately (i.e., `f x + f y`).
More concisely: For any additive homomorphism `f` from an additive type `α` to an additive type `β`, `f (x + y) = f x + f y` for all `x, y ∈ α`.
|
IsMulHom.comp
theorem IsMulHom.comp :
∀ {α : Type u} {β : Type v} [inst : Mul α] [inst_1 : Mul β] {γ : Type u_1} [inst_2 : Mul γ] {f : α → β} {g : β → γ},
IsMulHom f → IsMulHom g → IsMulHom (g ∘ f)
This theorem states that if you have two functions `f` and `g` such that `f` maps from type `α` to type `β` and `g` maps from type `β` to type `γ`, both of which are equipped with a multiplication operation, then if both `f` and `g` preserve the multiplicative structure of their respective domains (i.e., are multiplicative homomorphisms, or `IsMulHom`s), then their composition `(g ∘ f)` also preserves this multiplication operation. In other words, the composition of two multiplicative homomorphisms is also a multiplicative homomorphism.
More concisely: If `f : α → β` and `g : β → γ` are multiplicative homomorphisms, then their composition `g ∘ f` is also a multiplicative homomorphism.
|
IsAddGroupHom.comp
theorem IsAddGroupHom.comp :
∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddGroup β] {f : α → β},
IsAddGroupHom f → ∀ {γ : Type u_1} [inst_2 : AddGroup γ] {g : β → γ}, IsAddGroupHom g → IsAddGroupHom (g ∘ f)
This theorem states that if you have two additive group homomorphisms, one from a group (α) to a group (β), and the other from group (β) to a group (γ), then the composition of these two homomorphisms (g ∘ f), is also an additive group homomorphism. This holds for any types α, β, and γ that are additive groups. An additive group homomorphism is a function that preserves the group operation, in this case, addition.
More concisely: If f : α → β and g : β → γ are additive group homomorphisms, then their composition g ∘ f is an additive group homomorphism from α to γ.
|
IsMonoidHom.inv
theorem IsMonoidHom.inv :
∀ {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst_1 : CommGroup β] {f : α → β},
IsMonoidHom f → IsMonoidHom fun a => (f a)⁻¹
This theorem states that for any types α and β, where α is a type with multiplication and unit, β is a commutative group, and f is a function from α to β, if f preserves multiplication (that is, it is a monoid homomorphism), then the function that maps each element of α to the inverse of its image under f also preserves multiplication. In other words, the inverse of a monoid homomorphism remains a monoid homomorphism when the target is a commutative group.
More concisely: If f : α → β is a monoid homomorphism from a multiplicative monoid α to a commutative group β, then the function g : α → β defined by g(x) = inverse(f(x)) is also a monoid homomorphism.
|
MulEquiv.isMulHom
theorem MulEquiv.isMulHom :
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (h : M ≃* N), IsMulHom ⇑h := by
sorry
This theorem states that for any multiplicative isomorphism 'h' from a type 'M' to another type 'N', where both 'M' and 'N' are instances of the 'MulOneClass' (meaning they support multiplication and have a multiplicative identity), the function 'h' is a multiplicative homomorphism. In other words, for any elements 'a' and 'b' of 'M', the isomorphism 'h' preserves the multiplication operation, i.e., 'h(ab) = h(a)h(b)'. However, this theorem is marked as deprecated, indicating that it might not be recommended for use in new code.
More concisely: Given a multiplicative isomorphism h from a multiplicative identity type M to another multiplicative identity type N, h(ab) = h(a)h(b).
|
IsGroupHom.map_one
theorem IsGroupHom.map_one :
∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Group β] {f : α → β}, IsGroupHom f → f 1 = 1
This theorem statement says that for any two types `α` and `β` with group structures, if a function `f` from `α` to `β` is a group homomorphism, then `f` maps the identity element of the group `α` (denoted as `1` here) to the identity element of the group `β` (also denoted as `1` here). In other words, a group homomorphism preserves the identity element of groups.
More concisely: If `f` is a group homomorphism from type `α` to type `β`, then `f(1α) = 1β`, where `1α` is the identity element of `α` and `1β` is the identity element of `β`.
|
IsAddMonoidHom.isAddMonoidHom_mul_right
theorem IsAddMonoidHom.isAddMonoidHom_mul_right :
∀ {γ : Type u_1} [inst : NonUnitalNonAssocSemiring γ] (x : γ), IsAddMonoidHom fun y => y * x
This theorem states that for any element `x` in a non-unital, non-associative semiring `γ`, the function that multiplies `x` from the right is an additive monoid homomorphism. In other words, for any two elements `a` and `b` of the semiring, the function satisfies the properties `(a + b) * x = a * x + b * x` (preservation of addition) and `0 * x = 0` (preservation of zero). These are the defining properties of an additive monoid homomorphism.
More concisely: For any non-unital, non-associative semiring `γ` and its element `x`, the right multiplication by `x` is an additive monoid homomorphism.
|
RingHom.to_isMonoidHom
theorem RingHom.to_isMonoidHom :
∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S),
IsMonoidHom ⇑f
This theorem states that for any given rings `R` and `S` that are non-associative semirings, any ring homomorphism `f` from `R` to `S` is also a monoid homomorphism. In other words, the ring homomorphism preserves the monoid structure (the operation and the identity element) of the rings.
More concisely: Given any non-associative semirings `R` and `S` and a ring homomorphism `f` from `R` to `S`, `f` is also a monoid homomorphism preserving the ring operations and identity element.
|
Neg.isAddGroupHom
theorem Neg.isAddGroupHom : ∀ {α : Type u} [inst : AddCommGroup α], IsAddGroupHom Neg.neg
The theorem `Neg.isAddGroupHom` states that for any type `α` which is an instance of a commutative additive group, the negation operation is a homomorphism of the additive group. In other words, negation preserves the group operation of addition in a commutative additive group.
More concisely: For any commutative additive group `α`, the negation operation is a homomorphism of the additive group.
|
IsAddGroupHom.map_zero
theorem IsAddGroupHom.map_zero :
∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddGroup β] {f : α → β}, IsAddGroupHom f → f 0 = 0 := by
sorry
This theorem states that for any additive group homomorphism `f` from one additive group `α` to another additive group `β`, the homomorphism `f` maps the identity element of the first group (which is 0 in additive notation) to the identity element of the second group (also 0 in additive notation). In other words, any group homomorphism preserves the identity elements of the groups involved.
More concisely: For any additive group homomorphism `f` from group `α` to group `β`, `f(0) = 0`, where `0` denotes the identity element of each group.
|
IsMulHom.map_mul
theorem IsMulHom.map_mul :
∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Mul β] {f : α → β},
IsMulHom f → ∀ (x y : α), f (x * y) = f x * f y
This theorem states that a function `f` preserves multiplication if it is a multiplicative homomorphism. In other words, for any types `α` and `β` with multiplication (`Mul α` and `Mul β`), and a function `f` from `α` to `β`, if `f` is a multiplicative homomorphism (`IsMulHom f`), then applying `f` to the product of any two values `x` and `y` from `α` (`f (x * y)`) is the same as the product of the function applied to `x` and `y` separately (`f x * f y`).
More concisely: If `f` is a multiplicative homomorphism from type `α` with multiplication to type `β` with multiplication, then `f (x * y) = f x * f y` for all `x, y` in `α`.
|
Inv.isGroupHom
theorem Inv.isGroupHom : ∀ {α : Type u} [inst : CommGroup α], IsGroupHom Inv.inv
This theorem states that the inversion operation is a group homomorphism if the group under consideration is commutative. In other words, for any commutative group (denoted by the Type variable 'α'), the function that inverts each element of the group preserves the group structure. This means if you take any two elements of the group, the inverse of their product is equal to the product of their inverses. In mathematical notation, this can be expressed as: for all 'a' and 'b' in the group 'α', `(ab)^-1 = a^-1 * b^-1`.
More concisely: For any commutative group 'α', the group operation and inversion are connected such that `(a * b)^-1 = a^-1 * b^-1` for all 'a' and 'b' in 'α'.
|
AddEquiv.isAddHom
theorem AddEquiv.isAddHom :
∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (h : M ≃+ N), IsAddHom ⇑h := by
sorry
This theorem states that for any two types `M` and `N` that are instances of the `AddZeroClass` (i.e., they have the properties of addition and zero), if there is an additive isomorphism `h` between `M` and `N`, then `h` preserves addition. In other words, `h` is an `IsAddHom`, which means it satisfies the property of an additive homomorphism (preserving the operation of addition). This theorem is marked as deprecated, suggesting that there might be a newer or more preferred way to express this property in the Lean 4 library.
More concisely: If `h` is an additive isomorphism between type `M` and type `N` that are instances of `AddZeroClass`, then `h` preserves addition, that is, `h (a +\_m b) = h a +\_n h b` for all `a, b : M`.
|
IsAddHom.add
theorem IsAddHom.add :
∀ {α : Type u_2} {β : Type u_3} [inst : AddSemigroup α] [inst_1 : AddCommSemigroup β] {f g : α → β},
IsAddHom f → IsAddHom g → IsAddHom fun a => f a + g a
This theorem states that if we have two functions `f` and `g` that preserve addition (i.e., they are additive or "additive homomorphisms") from a semi-group `α` to a commutative semi-group `β`, then the function that maps an element `a` from `α` to the sum of `f(a)` and `g(a)` also preserves addition. In other words, the sum of two additive functions is also an additive function.
More concisely: If `f` and `g` are additive functions from a semi-group `α` to a commutative semi-group `β`, then the function `h(a) = f(a) + g(a)` is also an additive function.
|
IsGroupHom.injective_iff
theorem IsGroupHom.injective_iff :
∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Group β] {f : α → β},
IsGroupHom f → (Function.Injective f ↔ ∀ (a : α), f a = 1 → a = 1)
This theorem states that a group homomorphism, `f`, from one group `α` to another group `β`, is injective if and only if its kernel is trivial. In other words, `f` is a one-to-one function if for every element `a` in group `α`, `f(a) = 1` (the identity element in group `β`) implies that `a = 1` (the identity element in `α`). This theorem links the concept of function injectivity with the concept of a trivial kernel in the context of group theory.
More concisely: A group homomorphism between two groups is injective if and only if its kernel is the trivial subgroup.
|
IsAddMonoidHom.map_add'
theorem IsAddMonoidHom.map_add' :
∀ {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst_1 : AddZeroClass β] {f : α → β},
IsAddMonoidHom f → ∀ (x y : α), f (x + y) = f x + f y
This theorem states that if `f` is an additive monoid homomorphism from a type `α` to a type `β`, both equipped with the addition operation and zero element, then `f` preserves the addition operation. In other words, for any two elements `x` and `y` of type `α`, the image of their sum under `f` is equal to the sum of their images. This is expressed mathematically as `f(x + y) = f(x) + f(y)`.
More concisely: If `f` is an additive monoid homomorphism from `α` to `β`, then `f(x + y) = f(x) + f(y)` for all `x, y` in `α`.
|
IsMulHom.mul
theorem IsMulHom.mul :
∀ {α : Type u_2} {β : Type u_3} [inst : Semigroup α] [inst_1 : CommSemigroup β] {f g : α → β},
IsMulHom f → IsMulHom g → IsMulHom fun a => f a * g a
The theorem `IsMulHom.mul` states that for any types `α` and `β`, where `α` is a semigroup and `β` is a commutative semigroup, if we have two functions `f` and `g` from `α` to `β` that preserve multiplication (each individually does not alter the result of multiplication under transformation), then the combined function that maps an element of `α` under `f` and `g` and then multiplies the results also preserves multiplication. This holds when multiplication is defined in the target `β` in a commutative way (i.e., the order of multiplication doesn't matter).
More concisely: If `f` and `g` are functions from a semigroup `α` to a commutative semigroup `β` preserving multiplication, then their composition `f ∘ g` also preserves multiplication.
|
IsGroupHom.inv
theorem IsGroupHom.inv :
∀ {α : Type u_1} {β : Type u_2} [inst : Group α] [inst_1 : CommGroup β] {f : α → β},
IsGroupHom f → IsGroupHom fun a => (f a)⁻¹
This theorem states that the inverse of a group homomorphism is itself a group homomorphism, provided that the target group is commutative. In other words, if we have a function `f` from a group `α` to a commutative group `β` that preserves the group structure (i.e., `f` is a group homomorphism), then the function that maps each element of `α` to the inverse of its image under `f` in `β` is also a group homomorphism.
More concisely: If `f` is a group homomorphism from a group `α` to a commutative group `β`, then the function that maps each element `x` in `α` to the inverse of `f(x)` in `β` is a group homomorphism.
|
IsAddGroupHom.to_isAddMonoidHom
theorem IsAddGroupHom.to_isAddMonoidHom :
∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddGroup β] {f : α → β},
IsAddGroupHom f → IsAddMonoidHom f
The theorem states that for any additive group homomorphism `f` from an additive group `α` to another additive group `β`, `f` is also an additive monoid homomorphism. In other words, any function that preserves the group structure (addition and inverse) between two additive groups also preserves the structure of an additive monoid (addition and zero), as every group is also a monoid.
More concisely: For any additive group homomorphism between two additive groups, the function preserves the addition and zero of the underlying additive monoids.
|
IsMonoidHom.map_one
theorem IsMonoidHom.map_one :
∀ {α : Type u} {β : Type v} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α → β}, IsMonoidHom f → f 1 = 1
This theorem states that for any function `f` from a type `α` to another type `β`, if `f` is a monoid homomorphism (i.e., it preserves the multiplication operation and identity element of a monoid structure), then `f` maps the multiplicative identity of `α` (`1` in the context of numbers) to the multiplicative identity of `β`. This is a fundamental property of monoid homomorphisms in the context of algebraic structures.
More concisely: If `f` is a monoid homomorphism from type `α` to type `β`, then `f(1) = 1` where `1` denotes the multiplicative identities of `α` and `β`, respectively.
|
RingHom.to_isAddGroupHom
theorem RingHom.to_isAddGroupHom :
∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S), IsAddGroupHom ⇑f
This theorem states that for any two types `R` and `S` which have a ring structure, if `f` is a ring homomorphism from `R` to `S`, then `f` is also an additive group homomorphism. In other words, it shows that the addition operation in the domain ring `R` is preserved under the ring homomorphism `f` to the ring `S`. This is a fundamental property in algebraic structures known as rings.
More concisely: A ring homomorphism between rings `R` and `S` is an additive group homomorphism from `R` to `S`.
|
IsAddGroupHom.add
theorem IsAddGroupHom.add :
∀ {α : Type u_1} {β : Type u_2} [inst : AddGroup α] [inst_1 : AddCommGroup β] {f g : α → β},
IsAddGroupHom f → IsAddGroupHom g → IsAddGroupHom fun a => f a + g a
The theorem states that for any two functions `f` and `g` from an additive group `α` to a commutative additive group `β`, if both `f` and `g` preserve the group operation (that is, they are additive group homomorphisms), then their pointwise sum (i.e., the function that maps each element of `α` to the sum of its images under `f` and `g`) is also an additive group homomorphism. In other words, the sum of two additive group homomorphisms is itself an additive group homomorphism when the target group is commutative.
More concisely: If `f` and `g` are additive group homomorphisms from an additive group `α` to a commutative additive group `β`, then their pointwise sum is also an additive group homomorphism.
|
IsAddGroupHom.injective_iff
theorem IsAddGroupHom.injective_iff :
∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddGroup β] {f : α → β},
IsAddGroupHom f → (Function.Injective f ↔ ∀ (a : α), f a = 0 → a = 0)
The theorem `IsAddGroupHom.injective_iff` states that for any given types `α` and `β`, where `α` and `β` are additive groups, and for any function `f` from `α` to `β`, if `f` is an additive group homomorphism, then `f` is injective (meaning that if `f x = f y` then `x = y`) if and only if its kernel is trivial. Here, a trivial kernel means that if `f a = 0` for some `a` in `α`, then `a` must be `0`.
More concisely: For additive groups α and β, and a function f : α → β that is an additive group homomorphism, f is injective if and only if its kernel {a : α | f(a) = 0} consists only of the additive identity of α.
|
IsMonoidHom.comp
theorem IsMonoidHom.comp :
∀ {α : Type u} {β : Type v} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α → β},
IsMonoidHom f → ∀ {γ : Type u_1} [inst_2 : MulOneClass γ] {g : β → γ}, IsMonoidHom g → IsMonoidHom (g ∘ f)
This theorem states that if you have two monoid homomorphisms, one from a type `α` to a type `β` and the other from type `β` to a type `γ`, then the composition of these two functions (first apply `f`, then apply `g` to the result) is also a monoid homomorphism. A monoid homomorphism is a function between two monoids (sets equipped with an associative binary operation and an identity element) that preserves the binary operation and the identity.
More concisely: If `f` is a monoid homomorphism from `α` to `β` and `g` is a monoid homomorphism from `β` to `γ`, then their composition `g ∘ f` is a monoid homomorphism from `α` to `γ`.
|
IsGroupHom.mul
theorem IsGroupHom.mul :
∀ {α : Type u_1} {β : Type u_2} [inst : Group α] [inst_1 : CommGroup β] {f g : α → β},
IsGroupHom f → IsGroupHom g → IsGroupHom fun a => f a * g a
This theorem states that given two types `α` and `β`, where `α` is a group and `β` is a commutative group, and given two group homomorphisms `f` and `g` from `α` to `β`, the product of `f` and `g` (defined as the function which maps `a` in `α` to `f(a)*g(a)` in `β`) is also a group homomorphism. This is predicated on the commutativity of the target group `β`.
More concisely: Given groups `α` and `β` (with `β` commutative), and group homomorphisms `f : α → β` and `g : α → β`, their composition `h(a) = f(a) * g(a)` is also a group homomorphism from `α` to `β`.
|
MulEquiv.isMonoidHom
theorem MulEquiv.isMonoidHom :
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (h : M ≃* N), IsMonoidHom ⇑h := by
sorry
This theorem states that a multiplicative bijection between two monoids is a monoid homomorphism. In other words, if we have two structures (denoted by `M` and `N`, respectively) that have associative multiplication and an identity element (which are the properties of a structure called a monoid), and there is a bijective function `h` that preserves multiplication between `M` and `N`, then this function `h` is a monoid homomorphism. This theorem is deprecated and the use of `MulEquiv.toMonoidHom` is suggested instead for this functionality.
More concisely: A bijective multiplicative function between two monoids is a monoid homomorphism.
|
IsMonoidHom.map_mul'
theorem IsMonoidHom.map_mul' :
∀ {α : Type u} {β : Type v} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α → β},
IsMonoidHom f → ∀ (x y : α), f (x * y) = f x * f y
This theorem states that a monoid homomorphism has the property of preserving multiplication from one algebraic structure (monoid) to another. Specifically, given two types α and β, both equipped with multiplication and a multiplicative identity (as per the `MulOneClass` structure), and a function `f` from α to β, if `f` is a monoid homomorphism (`IsMonoidHom f`), then for any two elements `x` and `y` from α, the image under `f` of the product `x * y` is equal to the product of the images `f x * f y`. In other words, applying `f` to the product of `x` and `y` is the same as multiplying the results of applying `f` to `x` and `y` separately. This property is fundamental to the definition of a monoid homomorphism.
More concisely: Given two monoids (α, *1α) and (β, *1β) and a monoid homomorphism f : α → β, then for all x, y in α, f (x * y) = f x * f y.
|
IsAddGroupHom.map_neg
theorem IsAddGroupHom.map_neg :
∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddGroup β] {f : α → β},
IsAddGroupHom f → ∀ (a : α), f (-a) = -f a
The theorem `IsAddGroupHom.map_neg` states that for any two additive groups `α` and `β` and a function `f` from `α` to `β`, if `f` is an additive group homomorphism, then `f` maps the negation of any element in `α` to the negation of its image in `β`. In other words, for any element `a` in `α`, the result of applying `f` to `-a` (negative of `a`) is the same as the negative of `f(a)`.
More concisely: For any additive groups α and β and additive group homomorphism f from α to β, f maps the negation of any element in α to the negation of its image in β. That is, -f(a) = f(-a) for all a in α.
|
IsGroupHom.map_inv
theorem IsGroupHom.map_inv :
∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Group β] {f : α → β},
IsGroupHom f → ∀ (a : α), f a⁻¹ = (f a)⁻¹
This theorem states that for any group homomorphism `f` from a group `α` to another group `β`, the inverse of an element `a` in the domain group `α` is mapped to the inverse of the image of `a` in the codomain group `β`. In mathematical terms, if `f` is a group homomorphism, and `a` is an element in group `α`, then `f(a⁻¹) = (f(a))⁻¹`. This property is one of the defining characteristics of a group homomorphism.
More concisely: For any group homomorphism `f` and element `a` in a group, `f(a^(-1)) = (f(a))^(-1)`.
|
IsAddHom.to_isAddMonoidHom
theorem IsAddHom.to_isAddMonoidHom :
∀ {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst_1 : AddGroup β] {f : α → β},
IsAddHom f → IsAddMonoidHom f
This theorem states that for any function `f` mapping elements from a type `α` (with structure of an additive zero class) to a type `β` (with structure of an additive group), if `f` preserves addition (i.e., `f` is an additive homomorphism), then `f` is also an additive monoid homomorphism. In mathematical terms, if `f(x + y) = f(x) + f(y)` for all `x, y` in `α`, then `f` also preserves the zero element and is a monoid homomorphism.
More concisely: If `f` is an additive homomorphism from an additive zero class `α` to an additive group `β`, then `f` is an additive monoid homomorphism and preserves the additive zero element of `β`.
|
IsAddMonoidHom.isAddMonoidHom_mul_left
theorem IsAddMonoidHom.isAddMonoidHom_mul_left :
∀ {γ : Type u_1} [inst : NonUnitalNonAssocSemiring γ] (x : γ), IsAddMonoidHom fun y => x * y
This theorem states that for any given type `γ`, which is a non-unital, non-associative semiring, and any given element `x` of `γ`, the function that maps any element `y` of `γ` to the product `x*y` is an additive monoid homomorphism. In other words, left multiplication by `x` in this type of ring preserves the operations of an additive monoid.
More concisely: For any non-unital, non-associative semiring type `γ` and element `x` in `γ`, left multiplication by `x` is an additive monoid homomorphism.
|
IsMonoidHom.id
theorem IsMonoidHom.id : ∀ {α : Type u} [inst : MulOneClass α], IsMonoidHom id
This theorem states that the identity map is a monoid homomorphism. In more detail, for any type `α` that has multiplication and a multiplicative identity (i.e., is an instance of the `MulOneClass` class), the identity function (which leaves every element unchanged) is a monoid homomorphism. A monoid homomorphism is a function between two monoids that preserves the monoid structure, i.e., it preserves the multiplication operation and the identity element.
More concisely: The identity function is a homomorphism with respect to the multiplication operation in any monoid with an identity.
|
IsAddMonoidHom.id
theorem IsAddMonoidHom.id : ∀ {α : Type u} [inst : AddZeroClass α], IsAddMonoidHom id
This theorem states that for any type `α` that has an `AddZeroClass` instance (which means that `α` is equipped with an additive operation and a zero element), the identity map is an additive monoid homomorphism. In mathematical terms, the identity function preserves the operation of addition and maps the zero element of `α` to the zero element of `α`.
More concisely: For any type `α` with an `AddZeroClass` instance, the identity function is an additive monoid homomorphism. In other words, for all `x, y : α`, the equality `(id α) (x + y) = (id α) x + (id α) y` holds.
|
IsGroupHom.comp
theorem IsGroupHom.comp :
∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Group β] {f : α → β},
IsGroupHom f → ∀ {γ : Type u_1} [inst_2 : Group γ] {g : β → γ}, IsGroupHom g → IsGroupHom (g ∘ f)
This theorem states that if you have two group homomorphisms, then their composition is also a group homomorphism. More specifically, for any groups `α`, `β`, and `γ`, if `f` is a homomorphism from `α` to `β` and `g` is a homomorphism from `β` to `γ`, then the composition `g ∘ f` is a homomorphism from `α` to `γ`. In the language of category theory, this asserts the "composability" of homomorphisms, a fundamental property that makes the category of groups a category.
More concisely: If `f` is a group homomorphism from `α` to `β` and `g` is a group homomorphism from `β` to `γ`, then their composition `g ∘ f` is a group homomorphism from `α` to `γ`.
|
IsAddHom.id
theorem IsAddHom.id : ∀ {α : Type u} [inst : Add α], IsAddHom id
This theorem states that the identity map preserves addition for any type `α` that has an addition operation. This means that applying the identity map to the sum of two elements of `α` results in the same value as summing the results of applying the identity map to each element individually. In mathematical terms, for all `a` and `b` in `α`, `id(a + b) = id(a) + id(b)`.
More concisely: For all types `α` with an addition operation and all elements `a` and `b` in `α`, the identity function preserves addition, that is, `id(a + b) = id(a) + id(b)`.
|