MonoidHom.ext_iff
theorem MonoidHom.ext_iff :
∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] {f g : M →* N},
f = g ↔ ∀ (x : M), f x = g x
This theorem, `MonoidHom.ext_iff`, states that for any two monoid homomorphisms `f` and `g` from a type `M` to a type `N` (both equipped with the structures of a multiplicative monoid), the two homomorphisms are equal if and only if their outputs are equal for every input from type `M`. This theorem is deprecated, and `DFunLike.ext_iff` is recommended for use instead.
More concisely: Two multiplicative monoid homomorphisms from a type to another are equal if and only if they map equal elements to equal outputs.
|
map_div'
theorem map_div' :
∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : DivInvMonoid G]
[inst_2 : DivInvMonoid H] [inst_3 : MonoidHomClass F G H] (f : F),
(∀ (a : G), f a⁻¹ = (f a)⁻¹) → ∀ (a b : G), f (a / b) = f a / f b
This theorem, `map_div'`, states that for any types `G`, `H`, and `F`, given `G` and `H` are `DivInvMonoid`s (division and inversion monoids), `F` is a function-like structure from `G` to `H`, and `F` is also a `MonoidHomClass` (a class of homomorphisms between two monoids), then for any function `f` of type `F`, if `f` preserves the inversion operation (i.e., for every element `a` in `G`, applying `f` to the inverse of `a` yields the inverse of `f(a)`), then `f` also preserves the division operation. That is, for every pair of elements `a` and `b` in `G`, applying `f` to the result of dividing `a` by `b` yields the same result as dividing `f(a)` by `f(b)`. This is a property of homomorphisms between structures with division and inversion operations.
More concisely: If `F` is a homomorphism between `DivInvMonoid`s `G` and `H` that preserves inversions, then `F(a / b) = F(a) / F(b)` for all `a, b` in `G`.
|
AddMonoidHom.map_zero
theorem AddMonoidHom.map_zero :
∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N), f 0 = 0
The theorem `AddMonoidHom.map_zero` states that for any additive monoid homomorphism `f` mapping from a type `M` to a type `N` (with `M` and `N` being add zero classes, i.e., classes that include an additive identity element '0'), the image of 0 under `f` will be 0. In simpler terms, this theorem is asserting that an additive monoid homomorphism preserves the additive identity, that is, it maps the '0' element of the domain to the '0' element of the codomain.
More concisely: For any additive monoid homomorphism f from an add zero class M to an add zero class N, f(0) = 0.
|
MonoidHom.comp_assoc
theorem MonoidHom.comp_assoc :
∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_10} [inst : MulOneClass M] [inst_1 : MulOneClass N]
[inst_2 : MulOneClass P] [inst_3 : MulOneClass Q] (f : M →* N) (g : N →* P) (h : P →* Q),
(h.comp g).comp f = h.comp (g.comp f)
This theorem, `MonoidHom.comp_assoc`, states that for any three monoid morphisms `f`, `g`, and `h` where `f` is a morphism from a monoid `M` to a monoid `N`, `g` is a morphism from `N` to `P`, and `h` is a morphism from `P` to `Q` (all monoids with respect to some multiplication and unit operation), the composition of these morphisms is associative. In other words, if we first compose `h` with `g` and then compose the result with `f`, it is the same as if we first composed `g` with `f` and then composed the result with `h`. This is equivalent to the mathematical statement $(h \circ g) \circ f = h \circ (g \circ f)$ for all `f`, `g`, `h`.
More concisely: For any monoid morphisms $f : M \to N$, $g : N \to P$, and $h : P \to Q$, the associativity of composition holds: $(h \circ g) \circ f = h \circ (g \circ f)$.
|
map_zsmul'
theorem map_zsmul' :
∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : SubNegMonoid G]
[inst_2 : SubNegMonoid H] [inst_3 : AddMonoidHomClass F G H] (f : F),
(∀ (x : G), f (-x) = -f x) → ∀ (a : G) (n : ℤ), f (n • a) = n • f a
The theorem `map_zsmul'` states that for any types `G`, `H`, and `F`, if `F` can be injected into a function from `G` to `H`, both `G` and `H` have a subtraction and negation operation (i.e., they are `SubNegMonoid`s), and `F` can be treated as a homomorphism from an additive monoid `G` to another additive monoid `H` (i.e., `F` follows the `AddMonoidHomClass` rules), then for any instance `f` of `F`, if `f` preserves negation (i.e., mapping `f` to `-x` results in `-f x` for any `x` in `G`), `f` also preserves the scalar multiplication of an integer `n` with a `SubNegMonoid` element `a` (i.e., `f (n • a) = n • f a` for any `a` in `G` and any integer `n`).
More concisely: If `F` is an additive homomorphism from a subtraction and negation monoid `G` to another such monoid `H` that preserves negation, then `F` preserves scalar multiplication by integers.
|
map_inv
theorem map_inv :
∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : Group G] [inst_2 : DivisionMonoid H]
[inst_3 : MonoidHomClass F G H] (f : F) (a : G), f a⁻¹ = (f a)⁻¹
The theorem `map_inv` states that for any group `G` and any division monoid `H`, and for any type `F` that has an injective function-like coercion from `G` to `H`, if `F` is a group homomorphism from `G` to `H`, then this group homomorphism preserves the inverse operation. In other words, given any element `a` in `G`, the homomorphism applied to the inverse of `a` is equal to the inverse of the homomorphism applied to `a`. This is expressed in mathematical terms as `f(a⁻¹) = (f(a))⁻¹`.
More concisely: For any group homomorphism `f` from a group `G` to a division monoid `H` with an injective coercion from `G` to `H`, `f(a⁻¹) = (f(a))⁻¹` for all `a` in `G`.
|
MulHom.ext_iff
theorem MulHom.ext_iff :
∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] {f g : M →ₙ* N}, f = g ↔ ∀ (x : M), f x = g x := by
sorry
This theorem, now deprecated and recommended to be replaced by `DFunLike.ext_iff`, states that for any two multiplication homomorphisms `f` and `g` from a type `M` with multiplication to a type `N` also with multiplication, `f` and `g` are equal if and only if for all elements `x` of type `M`, the result of applying `f` to `x` is the same as the result of applying `g` to `x`. In other words, two multiplication homomorphisms are equal if they produce the same results when applied to the same inputs.
More concisely: Two multiplication homomorphisms from a type with multiplication to another type with multiplication are equal if and only if they agree on the multiplication of all elements.
|
OneHom.comp_assoc
theorem OneHom.comp_assoc :
∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_10} [inst : One M] [inst_1 : One N] [inst_2 : One P]
[inst_3 : One Q] (f : OneHom M N) (g : OneHom N P) (h : OneHom P Q), (h.comp g).comp f = h.comp (g.comp f)
This theorem states that the composition of monoid homomorphisms is associative. In other words, for any three monoid homomorphisms `f`, `g`, and `h` mapping between possibly different monoids `M`, `N`, `P`, and `Q`, first composing `g` with `h`, and then this composition with `f`, is the same as first composing `f` with `g` and then this composition with `h`. The monoids involved here are assumed to be one-monoids, which are monoids with a specified element acting as the identity.
More concisely: For any monoid homomorphisms `f : M -> N`, `g : N -> P`, and `h : Q -> P` between one-monoids, `(g ∘ h) ∘ f` equals `g ∘ (h ∘ f)`.
|
OneHom.coe_inj
theorem OneHom.coe_inj :
∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] ⦃f g : OneHom M N⦄, ⇑f = ⇑g → f = g
This theorem, `OneHom.coe_inj`, states that for any two types `M` and `N`, given that `M` and `N` are equipped with the structure of a `One` (i.e., they have an explicitly specified 'one' or identity element), and given two `OneHom` objects `f` and `g` (functions preserving the 'one' or identity element) from `M` to `N`, if the function application of `f` and `g` (denoted by `⇑f` and `⇑g`) are equal, then `f` and `g` themselves are equal. In other words, it demonstrates the injectivity of the function applied to `OneHom` objects. Note, however, that this theorem is deprecated, and `DFunLike.coe_injective` should be used instead.
More concisely: Given types `M` and `N` with a specified identity element, and `OneHom` functions `f` and `g` from `M` to `N`, if `⇑f = ⇑g`, then `f = g`.
|
map_zpow'
theorem map_zpow' :
∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : DivInvMonoid G]
[inst_2 : DivInvMonoid H] [inst_3 : MonoidHomClass F G H] (f : F),
(∀ (x : G), f x⁻¹ = (f x)⁻¹) → ∀ (a : G) (n : ℤ), f (a ^ n) = f a ^ n
The theorem `map_zpow'` states that for given types `G`, `H`, and `F`, if `F` is a function-like from `G` to `H` (`F` has an injective coercion to functions from `G` to `H`), `G` and `H` both have an instance of `DivInvMonoid` (a mathematical structure that combines a monoid with an operation of inversion), and `F` has an instance of `MonoidHomClass` (which means `F` is a homomorphism over the monoids `G` and `H`), then for any function `f` from `F`, if `f` preserves the inversion operation (i.e., the inversion of `f(x)` equals `f` of the inverse of `x`), then `f` also preserves the integer power operation. In other words, for any `a` in `G` and any integer `n`, applying `f` to `a` raised to the power `n` is the same as first applying `f` to `a` and then raising the result to the power `n`. This property is important in the theory of group homomorphisms.
More concisely: If `F` is a function-like from a group `G` to a group `H` that preserves the group operation and inversion, then `F` preserves the integer power operation.
|
OneHom.map_one'
theorem OneHom.map_one' :
∀ {M : Type u_10} {N : Type u_11} [inst : One M] [inst_1 : One N] (self : OneHom M N), self.toFun 1 = 1
This theorem states that for any types `M` and `N` that are equipped with a multiplicative identity (denoted as `One M` and `One N` respectively), a function between `M` and `N` that preserves this identity (termed a `OneHom`) will map the identity in `M` (represented as `1`) to the identity in `N` (also represented as `1`). In other words, if we have a function that respects the multiplicative identity, applying this function to the multiplicative identity of `M` will give us the multiplicative identity of `N`.
More concisely: Given types `M` and `N` with multiplicative identities `One M` and `One N`, and a function `f : M → N` that preserves multiplicative identities (`f (One M) = One N`), then `f (1 : M) = 1 : N`.
|
AddMonoidHom.ext_iff
theorem AddMonoidHom.ext_iff :
∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {f g : M →+ N},
f = g ↔ ∀ (x : M), f x = g x
This theorem states that for any two additive monoid homomorphisms `f` and `g` between two types `M` and `N` (where `M` and `N` are types with add zero classes), `f` and `g` are equal if and only if their outputs are equal for every input from type `M`. However, this theorem is deprecated and it is advised to use `DFunLike.ext_iff` instead.
More concisely: Two additive monoid homomorphisms between types with add zero classes are equal if and only if they map identical inputs to identical outputs.
|
MulHom.map_mul'
theorem MulHom.map_mul' :
∀ {M : Type u_10} {N : Type u_11} [inst : Mul M] [inst_1 : Mul N] (self : M →ₙ* N) (x y : M),
self.toFun (x * y) = self.toFun x * self.toFun y
This theorem states that a function, represented as `self`, which is a multiplicative homomorphism (abbreviated as `MulHom`) from one multiplication-carrying structure `M` to another one `N`, preserves the multiplication operation. In other words, for any elements `x` and `y` of the structure `M`, the result of applying `self` to the product of `x` and `y` (`self.toFun (x * y)`) is identical to the product of the results of applying `self` to `x` and `y` separately (`self.toFun x * self.toFun y`).
More concisely: For any multiplicative homomorphism `self` from multiplication-carrying structure `M` to `N`, `self (x * y) = self x * self y` for all `x, y` in `M`.
|
AddMonoidHom.congr_fun
theorem AddMonoidHom.congr_fun :
∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {f g : M →+ N},
f = g → ∀ (x : M), f x = g x
This theorem states that for any two additive monoid homomorphisms 'f' and 'g' from one type 'M' to another type 'N' (where 'M' and 'N' are types with an additive zero class structure), if 'f' and 'g' are equal, then the result of applying 'f' and 'g' to any element 'x' of type 'M' will also be equal. It's important to note that this theorem is deprecated and `DFunLike.congr_fun` should be used instead.
More concisely: For any additive monoid homomorphisms f and g from type M to type N with additive zero, if f = g, then for all x in M, f(x) = g(x).
|
map_one
theorem map_one :
∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : One M] [inst_1 : One N] [inst_2 : FunLike F M N]
[inst_3 : OneHomClass F M N] (f : F), f 1 = 1
The theorem `map_one` states that for any types `M`, `N`, and `F`, given that `M` and `N` have a one (unit) element (i.e., they are equipped with a `One` structure), and `F` is a function-like object from `M` to `N` (as stipulated by the `FunLike` structure), and `F` preserves the one element (as expressed by `OneHomClass`), then applying any `F` to the one element of `M` yields the one element of `N`. In short, this theorem asserts that, under the given conditions, the one element is preserved under `F`.
More concisely: If `M` and `N` are types with one elements and `F` is a function-like object from `M` to `N` preserving the one element, then `F (one_M) = one_N`.
|
MonoidHom.map_div
theorem MonoidHom.map_div :
∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : DivisionMonoid β] (f : α →* β) (g h : α),
f (g / h) = f g / f h
This theorem states that group homomorphisms preserve division. Specifically, for any two elements `g` and `h` from a group `α` and a homomorphism `f` from `α` to a division monoid `β`, the image of the division of `g` and `h` under `f` is the same as the division of the images of `g` and `h` under `f`. In mathematical terms, this can be written as `f(g / h) = f(g) / f(h)`.
More concisely: Given a group homomorphism `f` from group `α` to a division monoid `β`, `f(g / h) = f(g) / f(h)` for all `g, h` in `α`.
|
MonoidHom.map_mul'
theorem MonoidHom.map_mul' :
∀ {M : Type u_10} {N : Type u_11} [inst : MulOneClass M] [inst_1 : MulOneClass N] (self : M →* N) (x y : M),
self.toFun (x * y) = self.toFun x * self.toFun y
This theorem states that for any two types 'M' and 'N' that belong to a multiplicative monoid (i.e., they have a multiplication operation and an identity element), a monoid homomorphism from 'M' to 'N' preserves the multiplication operation. In other words, if you have two elements 'x' and 'y' from the monoid 'M', applying the homomorphism to the product of 'x' and 'y' ('x * y') is the same as multiplying the images of 'x' and 'y' (i.e., `self.toFun x * self.toFun y`).
More concisely: Given monoid homomorphisms f : M -> N between multiplicative monoids M and N, for all x, y in M, f(x * y) = f(x) * f(y).
|
AddMonoidHom.map_zsmul
theorem AddMonoidHom.map_zsmul :
∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : SubtractionMonoid β] (f : α →+ β) (g : α) (n : ℤ),
f (n • g) = n • f g
The theorem `AddMonoidHom.map_zsmul` states that for any additive group homomorphism `f` from an additive group `α` to a subtraction monoid `β`, any element `g` of `α`, and any integer `n`, the homomorphism `f` applied to `n` times `g` (denoted `n • g`) is equal to `n` times the homomorphism `f` applied to `g` (denoted `n • f g`). In other words, additive group homomorphisms preserve the operation of integer scaling.
More concisely: For any additive group homomorphism $f : \alpha \rightarrow \beta$ where $\beta$ is a subtraction monoid, and for all $g \in \alpha$ and integer $n$, we have $f(n \cdot g) = n \cdot f(g)$.
|
map_ne_zero_iff
theorem map_ne_zero_iff :
∀ {R : Type u_10} {S : Type u_11} {F : Type u_12} [inst : Zero R] [inst_1 : Zero S] [inst_2 : FunLike F R S]
[inst_3 : ZeroHomClass F R S] (f : F), Function.Injective ⇑f → ∀ {x : R}, f x ≠ 0 ↔ x ≠ 0
The theorem `map_ne_zero_iff` states that for all types `R`, `S`, and `F`, given that `R` and `S` have a zero element, `F` is a function-like structure from `R` to `S`, and `F` is a zero-preserving homomorphism, then for any function `f` of type `F`, if `f` is injective, then for all `x` of type `R`, `f(x)` is not zero if and only if `x` is not zero. In other words, an injective zero-preserving homomorphism sends non-zero elements to non-zero elements.
More concisely: An injective, zero-preserving homomorphism between two abelian groups maps non-zero elements to non-zero elements.
|
map_zsmul
theorem map_zsmul :
∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : AddGroup G]
[inst_2 : SubtractionMonoid H] [inst_3 : AddMonoidHomClass F G H] (f : F) (n : ℤ) (g : G), f (n • g) = n • f g
The theorem `map_zsmul` states that, for any types `G`, `H`, and `F`, if `F` has a structure of `FunLike` from `G` to `H`, `G` is an additive group, `H` is a subtraction monoid, and `F` is an additive monoid homomorphism from `G` to `H`, then any additive group homomorphism `f` from `G` to `H` preserves the operation of integer scaling. In other words, mapping an element `g` from `G` scaled by an integer `n` under `f` is the same as scaling the mapping of `g` under `f` by the same integer `n`. Formally, for all `f`, `n` and `g`, `f(n • g) = n • f(g)`.
More concisely: Given an additive group `G`, a subtraction monoid `H`, and an additive monoid homomorphism `F` from `G` to `H`, any additive group homomorphism `f` from `G` to `H` satisfies `f(n * g) = n * f(g)` for all `n` in `ℤ` and `g` in `G`.
|
MonoidHom.map_mul_inv
theorem MonoidHom.map_mul_inv :
∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : DivisionMonoid β] (f : α →* β) (g h : α),
f (g * h⁻¹) = f g * (f h)⁻¹
The theorem `MonoidHom.map_mul_inv` states that for any two elements `g` and `h` from a group `α`, and a group homomorphism `f` from `α` to a division monoid `β`, the value of `f` at the product of `g` and the inverse of `h` (`g * h⁻¹`) is equal to the product of `f(g)` and the inverse of `f(h)` (`f(g) * (f(h))⁻¹`). In simpler terms, this theorem asserts that group homomorphisms preserve the operation of division.
More concisely: For any group homomorphism from a group to a division monoid, the image of the product of two group elements and their inverses equals the product of their images and the inverses of those images.
|
AddMonoidHom.id_comp
theorem AddMonoidHom.id_comp :
∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N),
(AddMonoidHom.id N).comp f = f
This theorem states that for any additive monoids `M` and `N`, and for any additive monoid morphism `f` from `M` to `N`, composing `f` with the identity map on `N` yields `f` itself. In other words, if we first apply the morphism `f`, and then apply the identity transformation, the overall effect is the same as just applying `f`. This is consistent with the mathematical concept of an identity function, which leaves its argument unchanged.
More concisely: For any additive monoid morphism `f` from `M` to `N`, the composition `f ∘ id_N` equals `f`, where `id_N` is the identity map on `N`.
|
MonoidHom.coe_mk
theorem MonoidHom.coe_mk :
∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : OneHom M N)
(hmul : ∀ (x y : M), f.toFun (x * y) = f.toFun x * f.toFun y), ⇑{ toOneHom := f, map_mul' := hmul } = ⇑f
This theorem states that for any two types `M` and `N` which both are instances of the `MulOneClass` (meaning they support multiplication and have a multiplicative identity), given a homomorphism `f` from `M` to `N` that preserves the identity, and a proof `hmul` that `f` also preserves multiplication, the function obtained by applying the coercion function `⇑` (which extracts the function part from the homomorphism) to the `MonoidHom` created from `f` and `hmul` is the same as the function obtained by applying `⇑` directly to `f`. In simpler terms, creating a `MonoidHom` from `f` and then extracting the function from it gives us back the original function `f`.
More concisely: For any homomorphism `f` between multiplicative monoids `M` and `N` preserving identity and multiplication, the extracted function from the `MonoidHom` construction is equal to `f` itself.
|
AddMonoidHom.ext
theorem AddMonoidHom.ext :
∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] ⦃f g : M →+ N⦄,
(∀ (x : M), f x = g x) → f = g
The theorem `AddMonoidHom.ext` states that for any two additive monoid homomorphisms `f` and `g` from an add-zero class `M` to another add-zero class `N`, if for every element `x` in `M`, `f(x)` is equal to `g(x)`, then `f` is equal to `g`. In other words, two additive monoid homomorphisms are considered identical if they produce the same result for each element of the domain.
More concisely: If two additive monoid homomorphisms between add-zero classes map the same element to the same image, then they are equal.
|
AddHom.congr_arg
theorem AddHom.congr_arg :
∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : AddHom M N) {x y : M}, x = y → f x = f y := by
sorry
This theorem, `AddHom.congr_arg`, states that for any two types `M` and `N` that have addition defined on them, and for any addition-preserving function `f` from `M` to `N`, if two elements `x` and `y` in `M` are equal, then their images under the function `f` are also equal. In other words, if `x = y`, then `f(x) = f(y)`. Note that this theorem is deprecated and it's recommended to use `DFunLike.congr_arg` instead.
More concisely: If `f` is an addition-preserving function between abelian groups `M` and `N`, then for all `x, y ∈ M`, `x = y` implies `f(x) = f(y)`.
|
ZeroHom.congr_arg
theorem ZeroHom.congr_arg :
∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (f : ZeroHom M N) {x y : M}, x = y → f x = f y
This theorem, `ZeroHom.congr_arg`, states that for any two types `M` and `N` that have a zero element (denoted by `inst : Zero M` and `inst_1 : Zero N`), and for any zero-preserving function `f` from `M` to `N` (denoted by `f : ZeroHom M N`), if two elements `x` and `y` of `M` are equal (i.e., `x = y`), then their images under the function `f` are also equal (i.e., `f x = f y`). Note that this theorem is deprecated, and it is recommended to use `DFunLike.congr_arg` instead.
More concisely: If `f` is a zero-preserving function from type `M` to type `N`, and `x` and `y` are equal elements of `M`, then `f(x)` and `f(y)` are equal elements of `N`.
|
MonoidHom.congr_fun
theorem MonoidHom.congr_fun :
∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] {f g : M →* N},
f = g → ∀ (x : M), f x = g x
This theorem, `MonoidHom.congr_fun`, states that for any two monoid homomorphisms `f` and `g` from one monoid `M` to another monoid `N`, if `f` is equal to `g`, then for any element `x` of `M`, the result of applying `f` to `x` is equal to the result of applying `g` to `x`. Here, monoids `M` and `N` are types possessing the structure of a muliplicative monoid, i.e., they have an operation "mul" that is associative and an element "one" that is the identity for this operation. Note that this theorem is deprecated, and `DFunLike.congr_fun` should be used instead.
More concisely: For any monoid homomorphisms `f` and `g` from a monoid `M` to a monoid `N` with identity elements `one_M` and `one_N`, respectively, if `f = g`, then for all `x` in `M`, `f x = g x`.
|
MulHomClass.map_mul
theorem MulHomClass.map_mul :
∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} [inst : Mul M] [inst_1 : Mul N]
[inst_2 : FunLike F M N] [self : MulHomClass F M N] (f : F) (x y : M), f (x * y) = f x * f y
The theorem `MulHomClass.map_mul` states that for any types `F`, `M`, and `N`, if `M` and `N` have a multiplication operation, `F` is a function-like type from `M` to `N`, and `F` is an instance of `MulHomClass` (i.e., it is a multiplication-preserving function), then for any function `f` of type `F` and any elements `x` and `y` of type `M`, the result of applying `f` to the product of `x` and `y` is equal to the product of the results of applying `f` to `x` and `f` to `y` individually. In other words, `f` preserves the multiplication operation: `f(x * y) = f(x) * f(y)`.
More concisely: For any types `M` with multiplication, and `F` a multiplication-preserving function from `M` to `M`, `F(x * y) = F(x) * F(y)` for all `x, y` in `M`.
|
map_add
theorem map_add :
∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
[inst_3 : AddHomClass F M N] (f : F) (x y : M), f (x + y) = f x + f y
The theorem `map_add` states that for all types `M`, `N`, and `F`, if `M` and `N` are equipped with addition operation, `F` is a function-like object from `M` to `N`, and `F` is an additive homomorphism (as specified by `AddHomClass F M N`), then for any function `f` of type `F` and any elements `x` and `y` of type `M`, the image of the sum `x + y` under `f` is equal to the sum of the images of `x` and `y` under `f`. In mathematical notation, this can be written as `f(x + y) = f(x) + f(y)`, which is the defining property of an additive homomorphism.
More concisely: For any additive homomorphism F from type M to type N and any elements x, y of type M, we have F(x + y) = F(x) + F(y).
|
AddMonoidHom.map_nsmul
theorem AddMonoidHom.map_nsmul :
∀ {M : Type u_4} {N : Type u_5} [inst : AddMonoid M] [inst_1 : AddMonoid N] (f : M →+ N) (a : M) (n : ℕ),
f (n • a) = n • f a
This theorem states that for any two types `M` and `N` that are additive monoids, any additive monoid homomorphism `f` from `M` to `N`, any element `a` of `M`, and any natural number `n`, the result of applying `f` to `n` times `a` in `M` is equal to `n` times the result of applying `f` to `a`. In other words, the homomorphism preserves the operation of scalar multiplication by a natural number.
More concisely: For any additive monoids M and N, any additive monoid homomorphism f from M to N, and any natural number n and element a in M, we have f(na) = n(fa).
|
OneHom.congr_fun
theorem OneHom.congr_fun :
∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] {f g : OneHom M N}, f = g → ∀ (x : M), f x = g x
This theorem, `OneHom.congr_fun`, states that for any two instances `f` and `g` of `OneHom` between the same types `M` and `N`, where `M` and `N` both have an instance of `One` (or a multiplicative identity), if `f` and `g` are equal, then their output for any input `x` from `M` is also equal. In other words, if two `OneHom` instances are the same, they behave the same way for every input. Note: this theorem is deprecated, and it's recommended to use `DFunLike.congr_fun` instead.
More concisely: If `f` and `g` are equal instances of `OneHom` from type `M` to type `N`, where `M` and `N` have a multiplicative identity, then for all `x` in `M`, `f x = g x`.
|
ZeroHom.ext
theorem ZeroHom.ext :
∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] ⦃f g : ZeroHom M N⦄,
(∀ (x : M), f x = g x) → f = g
This theorem states that for any two zero homomorphisms `f` and `g` from a type `M` with a zero element to a type `N` also with a zero element, if `f` and `g` have the same value for every `x` in `M`, then `f` is equal to `g`. A zero homomorphism is a function that preserves the zero element, i.e., it maps the zero of `M` to the zero of `N`.
More concisely: If two zero homomorphisms from a type with a zero element to another type with a zero element agree on all elements, then they are equal.
|
MulHom.congr_fun
theorem MulHom.congr_fun :
∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] {f g : M →ₙ* N}, f = g → ∀ (x : M), f x = g x := by
sorry
This theorem, `MulHom.congr_fun`, states that for any two multiplication homomorphisms `f` and `g` from a type `M` with multiplication to another type `N` with multiplication, if `f` equals `g`, then the result of applying `f` to any element `x` from `M` will be equal to the result of applying `g` to the same `x`. Note that this theorem is deprecated and it is recommended to use `DFunLike.congr_fun` instead.
More concisely: If `f` and `g` are equal multiplication homomorphisms from a type `M` to a type `N` with multiplication, then for all `x` in `M`, `f x = g x`.
|
MonoidHom.map_one
theorem MonoidHom.map_one :
∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N), f 1 = 1
This theorem states that for any given monoid homomorphism `f` from a type `M` to a type `N`, where `M` and `N` are both instances of the `MulOneClass` (which means they have a multiplication operation and an identity element `1`), the image of the identity element under the homomorphism `f` is the identity element in `N`. In other words, if `f` is a monoid homomorphism, then applying `f` to the identity element `1` in `M` results in the identity element `1` in `N`.
More concisely: For any monoid homomorphism f from a monoid (M, ∧, 1) to a monoid (N, ⊤, 1), the image of the identity element 1 under f is the identity element 1 in N.
|
map_div
theorem map_div :
∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : Group G] [inst_2 : DivisionMonoid H]
[inst_3 : MonoidHomClass F G H] (f : F) (a b : G), f (a / b) = f a / f b
The theorem `map_div` states that for any groups `G` and `H`, and for any type `F` that is a function-like from `G` to `H`, if `F` is a homomorphism between the monoids `G` and `H`, and `H` is a division monoid, then this homomorphism preserves the division operation. In other words, applying the homomorphism to the quotient of two elements from `G` results in the same value as the quotient of the images of the two elements under the homomorphism.
More concisely: If `F : G →* H` is a homomorphism of monoids from a group `G` into a division monoid `H`, then `F (x / y) = F x / F y` for all `x, y ∈ G`.
|
AddHom.ext
theorem AddHom.ext :
∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] ⦃f g : AddHom M N⦄,
(∀ (x : M), f x = g x) → f = g
This theorem states that for any two additive homomorphisms `f` and `g` from a type `M` with addition to a type `N` with addition, if for every element of type `M`, `f` and `g` have the same result, then `f` and `g` are the same homomorphism. In essence, it provides a criterion for the equality of two additive homomorphisms based on their actions on the elements of the domain.
More concisely: If two additive homomorphisms from a commutative additive group `M` to a commutative additive group `N` agree on every element of `M`, then they are equal.
|
MonoidHom.id_comp
theorem MonoidHom.id_comp :
∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N),
(MonoidHom.id N).comp f = f
The theorem `MonoidHom.id_comp` states that for any monoid morphism `f` from a monoid `M` to another monoid `N`, the composition of `f` with the identity map on `N` is just `f` itself. Here, the monoids `M` and `N` can be any types equipped with a multiplication operation and a distinguished "one" element, and `f` is any function that preserves these structures (i.e., a monoid homomorphism). This is an instance of the general principle in mathematics that composing any function with the identity function leaves the original function unchanged.
More concisely: For any monoid homomorphism `f` from monoid `M` to monoid `N`, `f ∘ id_N = f`.
|
MonoidHom.ext
theorem MonoidHom.ext :
∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] ⦃f g : M →* N⦄,
(∀ (x : M), f x = g x) → f = g
This theorem, `MonoidHom.ext`, states that for any two types `M` and `N` that are instances of the `MulOneClass` (which means they have multiplication and one-element, i.e., they are monoids), if we have two homomorphisms `f` and `g` from `M` to `N`, and for all elements `x` of `M`, `f(x)` is equal to `g(x)`, then `f` and `g` must be the same homomorphism. In simpler terms, two homomorphisms between two monoids are equivalent if they give the same result for every element of the source monoid.
More concisely: If `M` and `N` are monoids, and `f` and `g` are homomorphisms from `M` to `N` such that `f(x) = g(x)` for all `x` in `M`, then `f` and `g` are equal.
|
OneHomClass.map_one
theorem OneHomClass.map_one :
∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} [inst : One M] [inst_1 : One N]
[inst_2 : FunLike F M N] [self : OneHomClass F M N] (f : F), f 1 = 1
The theorem `OneHomClass.map_one` asserts that for all types `F`, `M`, and `N`, if `M` and `N` are equipped with the structure of a one-object (i.e., they have a specified element `1`), `F` is a function-like object from `M` to `N`, and `F` is a one-homomorphism (i.e., it preserves the `1` element under the function), then applying `F` to `1` in `M` results in `1` in `N`. In other words, a one-homomorphism maps the `1` element of `M` to the `1` element of `N`.
More concisely: Given types `M` and `N` with specified elements `1`, a function-like object `F` from `M` to `N` that is a one-homomorphism maps `1` in `M` to `1` in `N`.
|
MulHom.congr_arg
theorem MulHom.congr_arg :
∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) {x y : M}, x = y → f x = f y := by
sorry
This theorem, which is labelled as deprecated and suggests the use of `DFunLike.congr_arg` instead, states that for any two types `M` and `N` that have multiplication defined on them and a multiplication-preserving function `f` from `M` to `N`, if two elements `x` and `y` from `M` are equal, then their images under `f` are also equal. This property is a fundamental characteristic of functions and is known as function congruence.
More concisely: If `f` is a function between types `M` and `N` that preserves multiplication, and `x` and `y` are equal elements of `M`, then `f x` and `f y` are equal elements of `N`.
|
map_mul_inv
theorem map_mul_inv :
∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : Group G] [inst_2 : DivisionMonoid H]
[inst_3 : MonoidHomClass F G H] (f : F) (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
The theorem `map_mul_inv` states that for any types `G`, `H`, and `F`, if `F` has a function-like structure from `G` to `H`, `G` is a group, `H` is a division monoid, and `F` serves as a monoid homomorphism from `G` to `H`, then for any instance `f` of type `F` and any elements `a` and `b` of `G`, applying `f` to the division of `a` and `b` in `G` is equivalent to the division of the images of `a` and `b` under `f` in `H`. In other words, a group homomorphism preserves the operation of division.
More concisely: For any group G, division monoid H, and monoid homomorphism F from G to H, the division of F(a) and F(b) in H equals F(a ^-1 * a) for all a, b in G. (Here, * denotes the group operation in G and ^-1 denotes the multiplicative inverse in G.)
|
map_eq_one_iff
theorem map_eq_one_iff :
∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : One M] [inst_1 : One N] [inst_2 : FunLike F M N]
[inst_3 : OneHomClass F M N] (f : F), Function.Injective ⇑f → ∀ {x : M}, f x = 1 ↔ x = 1
The theorem `map_eq_one_iff` states that for any types `M`, `N`, and `F`, given a one-structure on `M` and `N`, and a function-like structure from `M` to `N`, if `F` is also a `OneHomClass` and `f` is an injective function from `M` to `N`, then for any element `x` of `M`, `f` maps `x` to `1` if and only if `x` is `1`.
In mathematical terms, this theorem states that if `f: M → N` is an injective homomorphism preserving the one-element under the given structures, then an element `x` in `M` gets mapped to the identity element in `N` if and only if the element itself is the identity element in `M`.
More concisely: Given types `M` and `N`, one-structures `one_M` and `one_N`, a function-like structure `F` from `M` to `N`, an injective homomorphism `f: M → N` as a `OneHomClass` preserving `one_M` and `one_N`, then `f x = one_N` if and only if `x = one_M`.
|
MonoidHom.map_exists_left_inv
theorem MonoidHom.map_exists_left_inv :
∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : MulOneClass M] [inst_1 : MulOneClass N]
[inst_2 : FunLike F M N] [inst_3 : MonoidHomClass F M N] (f : F) {x : M}, (∃ y, y * x = 1) → ∃ y, y * f x = 1
The theorem `MonoidHom.map_exists_left_inv` states that for any given types `M`, `N`, and `F`, where `M` and `N` have multiplication and identity elements (`MulOneClass`), and `F` is a function type from `M` to `N` (`FunLike F M N`) acting like a monoid homomorphism (`MonoidHomClass F M N`). Then for any function `f` of type `F` and any element `x` of type `M`, if `x` has a left inverse (that is, there exists a `y` such that `y*x = 1`), then the image of `x` under `f` (i.e., `f x`) also has a left inverse in `N` (there exists a `y` such that `y * f x = 1`). Note that this is only for elements invertible on the left side, for elements invertible on both sides, the theorem `IsUnit.map` should be used.
More concisely: If `F` is a monoid homomorphism from the multiplicative monoid `M` to the multiplicative monoid `N`, and `x` in `M` has a left inverse, then `f x` in `N` has a left inverse.
|
AddHom.coe_inj
theorem AddHom.coe_inj :
∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] ⦃f g : AddHom M N⦄, ⇑f = ⇑g → f = g
This theorem, `AddHom.coe_inj`, is deprecated and it's recommended to use `DFunLike.coe_injective` instead. The theorem states that for any two additive homomorphisms `f` and `g` from a type `M` with addition to a type `N` with addition, if the function represented by `f` is equal to the function represented by `g`, then `f` is equal to `g`.
More concisely: If `f` and `g` are additive homomorphisms from a group `M` to a group `N`, then `f = g` implies `f(x) = g(x)` for all `x` in `M`.
|
ZeroHom.coe_inj
theorem ZeroHom.coe_inj :
∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] ⦃f g : ZeroHom M N⦄, ⇑f = ⇑g → f = g
The theorem `ZeroHom.coe_inj` states that for any two zero homomorphisms `f` and `g` from one type `M` to another type `N` (both endowed with a zero structure), if the function obtained by applying the coercion function to `f` is equal to the function obtained by applying the coercion function to `g`, then `f` and `g` are equal. However, this theorem is deprecated, and `DFunLike.coe_injective` should be used instead.
More concisely: If two zero homomorphisms from type `M` to type `N` with zero structures have coercions to the same function, then they are equal. (Deprecated: use `DFunLike.coe_injective` instead.)
|
MulHom.map_mul
theorem MulHom.map_mul :
∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (a b : M), f (a * b) = f a * f b := by
sorry
This theorem states that for any two types `M` and `N`, if both of them have a multiplication operation and there exists a multiplication-preserving function `f` (also known as a multiplicative homomorphism) from `M` to `N`, then for any two elements `a` and `b` of `M`, the result of applying `f` to the product `a * b` is the same as the product of applying `f` to `a` and `b` individually. In other words, the function `f` preserves the multiplication operation under its mapping from `M` to `N`.
More concisely: If `f` is a multiplicative homomorphism from type `M` with multiplication `*` to type `N` with multiplication `�� /******/`, then for all `a, b` in `M`, `f(a * b) = f(a) �� /******/ f(b)`.
|
MonoidHom.map_pow
theorem MonoidHom.map_pow :
∀ {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N) (a : M) (n : ℕ),
f (a ^ n) = f a ^ n
This theorem states that for any two types `M` and `N`, which both have a `Monoid` structure, and for any homomorphism `f` from `M` to `N`, `f` maps the `n`th power of an element `a` from `M` to the `n`th power of the image of `a` under `f` in `N`. Essentially, this theorem is conveying that a monoid homomorphism preserves the power operation.
More concisely: For any monoid homomorphisms $f : M \to N$ between monoids $M$ and $N$, and any $a \in M$ and $n \in \mathbb{N}$, we have $f(a^n) = (f(a))^n$.
|
AddMonoidHom.id_apply
theorem AddMonoidHom.id_apply : ∀ (M : Type u_10) [inst : AddZeroClass M] (x : M), (AddMonoidHom.id M) x = x
This theorem states that for any type `M` that is an instance of the `AddZeroClass` (in other words, `M` is an additive monoid), the identity map on this additive monoid, when applied to any element `x` of `M`, returns `x` itself. This is analogous to the mathematical property where the identity map (function) on any mathematical structure (like a set or a group) leaves each element unchanged.
More concisely: For any additive monoid M, the identity function maps each element x of M to x itself.
|
MonoidHom.coe_inj
theorem MonoidHom.coe_inj :
∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] ⦃f g : M →* N⦄, ⇑f = ⇑g → f = g
This theorem, `MonoidHom.coe_inj`, states that for two types `M` and `N` with multiplication and one as a binary operation (i.e., they are instances of the `MulOneClass`), if we have two multiplication-preserving functions (monoid homomorphisms) `f` and `g` from `M` to `N`, and if these two functions are equal when used as functions (coerced to a function type with the `⇑` operator), then the original monoid homomorphisms `f` and `g` must also be equal. This theorem has been deprecated and it is recommended to use `DFunLike.coe_injective` instead.
More concisely: If `f` and `g` are equal as functions and are multiplication-preserving homomorphisms from a monoid `M` to a monoid `N`, then `f` and `g` are equal as homomorphisms.
|
AddHom.map_add'
theorem AddHom.map_add' :
∀ {M : Type u_10} {N : Type u_11} [inst : Add M] [inst_1 : Add N] (self : AddHom M N) (x y : M),
self.toFun (x + y) = self.toFun x + self.toFun y
This theorem states that for any two types `M` and `N` that have addition defined on them, if there is a function (`self`) from `M` to `N` that obeys the properties of an addition homomorphism (`AddHom`), then this function preserves the addition operation. That is, applying the function to the sum of two elements `x` and `y` from `M` is the same as applying the function to each element separately and then adding the results in `N`. In mathematical notation, this could be represented as `f(x + y) = f(x) + f(y)`, where `f` is the function from `M` to `N`.
More concisely: If `f : M → N` is an additive homomorphism between types `M` and `N` with addition, then `f(x + y) = f(x) + f(y)` for all `x, y ∈ M`.
|
AddHom.map_add
theorem AddHom.map_add :
∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : AddHom M N) (a b : M), f (a + b) = f a + f b
This theorem, named `AddHom.map_add`, states that for all types `M` and `N` that have an addition operation (`Add M` and `Add N`), a function `f` that is an additive homomorphism (`AddHom M N`) preserves the addition operation. Specifically, for any two elements `a` and `b` of type `M`, applying the function `f` to the sum of `a` and `b` (`f (a + b)`) is the same as summing the individual results of applying `f` to `a` and `b` (`f a + f b`).
More concisely: For any additive homomorphisms `f : Add M → Add N` between abelian groups `M` and `N`, `f (a + b) = f a + f b` for all `a, b ∈ M`.
|
ZeroHom.map_zero
theorem ZeroHom.map_zero :
∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (f : ZeroHom M N), f 0 = 0
This theorem states that, for any two types `M` and `N` that have a zero element (denoted by the `Zero M` and `Zero N` instances respectively), any `ZeroHom` (zero-preserving function) `f` from `M` to `N` will map the zero element of `M` to the zero element of `N`. In mathematical terms, given a zero-preserving function `f`, we have `f(0) = 0`.
More concisely: If `f` is a zero-preserving function from type `M` to type `N` with zero elements `Zero M` and `Zero N`, then `f (Zero M) = Zero N`.
|
MulHom.coe_inj
theorem MulHom.coe_inj :
∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] ⦃f g : M →ₙ* N⦄, ⇑f = ⇑g → f = g
This theorem, `MulHom.coe_inj`, states that for any two multiplicatively homomorphic functions `f` and `g` from a type `M` with a multiplication operation to a type `N` with a multiplication operation, if the coercion of `f` to a function equals the coercion of `g` to a function, then `f` and `g` are equal. In other words, the coercion to a function is injective (has a one-to-one correspondence) for multiplicative homomorphisms. However, this theorem is deprecated and the use of `DFunLike.coe_injective` is recommended instead.
More concisely: If two multiplicatively homomorphic functions from type `M` to type `N` have equal function coercions, then they are equal.
|
AddMonoidHom.map_add
theorem AddMonoidHom.map_add :
∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N) (a b : M),
f (a + b) = f a + f b
The theorem `AddMonoidHom.map_add` states that given any two types `M` and `N` that are additive monoids (i.e., they have a zero element and an operation `+` that is associative and has a zero element as its identity), if a function `f` is a homomorphism between these two additive monoids, then for any elements `a` and `b` from `M`, the image of the sum `a + b` under `f` is equal to the sum of the images of `a` and `b` under `f`. This property is key in defining what it means for a function to be a homomorphism between additive monoids.
More concisely: Given additive monoids M and N and a homomorphism f between them, for all a, b in M, f(a + b) = f(a) + f(b).
|
MonoidHom.cancel_right
theorem MonoidHom.cancel_right :
∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : MulOneClass M] [inst_1 : MulOneClass N]
[inst_2 : MulOneClass P] {g₁ g₂ : N →* P} {f : M →* N},
Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
The theorem `MonoidHom.cancel_right` states that for any three types `M`, `N`, and `P` that have the structure of a monoid (i.e., a set equipped with an associative binary operation and an identity element), given two monoid homomorphisms `g₁` and `g₂` from `N` to `P`, and another monoid homomorphism `f` from `M` to `N`, if `f` is surjective (i.e., for every element in `N`, there is an element in `M` such that applying `f` to this element gives the element in `N`), then the composition of `g₁` and `f` is equal to the composition of `g₂` and `f` if and only if `g₁` is equal to `g₂`. This theorem is a statement about the cancellation property of compositions of monoid homomorphisms when the second function is surjective.
More concisely: Given monoid homomorphisms `f: M -> N`, `g₁, g₂: N -> P`, and `f` surjective, `g₁ ∘ f = g₂ ∘ f` if and only if `g₁ = g₂`.
|
OneHom.ext_iff
theorem OneHom.ext_iff :
∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] {f g : OneHom M N}, f = g ↔ ∀ (x : M), f x = g x
The theorem `OneHom.ext_iff` states that for any two instances `f` and `g` of `OneHom` (which is a type of function between types `M` and `N` with a multiplicative identity), `f` and `g` are equal if and only if they give the same result for every element of type `M`. This theorem is deprecated, and the use of `DFunLike.ext_iff` is recommended instead.
More concisely: For any functions `f` and `g` between types `M` and `N` that are instances of `OneHom`, they are equal if and only if they map every element of `M` to the same element in `N`.
|
map_nsmul
theorem map_nsmul :
∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : AddMonoid G] [inst_2 : AddMonoid H]
[inst_3 : AddMonoidHomClass F G H] (f : F) (n : ℕ) (a : G), f (n • a) = n • f a
The theorem `map_nsmul` states that for any types `G`, `H`, and `F`, given that `F` is a function-like type from `G` to `H`, and both `G` and `H` are additive monoids, and `F` is a homomorphism class from `G` to `H`, then for any function `f` of type `F`, natural number `n`, and element `a` of `G`, the result of applying `f` to the `n`-fold self-addition of `a` is equal to the `n`-fold self-addition of the result of applying `f` to `a`. In mathematical terms, if `F` is a homomorphism between the additive monoids `G` and `H`, then `f(na) = nf(a)` for all `n` in the natural numbers and `a` in `G`.
More concisely: For any homomorphism `F` between additive monoids `G` and `H`, `F(na) = nF(a)` for all natural numbers `n` and elements `a` in `G`.
|
AddMonoidHom.map_add'
theorem AddMonoidHom.map_add' :
∀ {M : Type u_10} {N : Type u_11} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (self : M →+ N) (x y : M),
self.toFun (x + y) = self.toFun x + self.toFun y
This theorem, named 'AddMonoidHom.map_add', states that for any two types `M` and `N` which are both instances of the `AddZeroClass`, any function `self` that maps elements of `M` to elements of `N` preserves the addition operation. More specifically, for any two elements `x` and `y` in `M`, applying the function `self` to the sum of `x` and `y` gives the same result as adding the results of applying `self` to `x` and `y` separately. This property is fundamental in the field of group theory and abstract algebra.
More concisely: Given functions `self : M -> N` between additive types `M` and `N`, and any `x, y : M`, we have `self (x + y) = self x + self y`.
|
AddMonoidHom.coe_inj
theorem AddMonoidHom.coe_inj :
∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] ⦃f g : M →+ N⦄, ⇑f = ⇑g → f = g
This theorem, `AddMonoidHom.coe_inj`, states that for any two additive monoid homomorphisms `f` and `g` from an additive monoid `M` to another additive monoid `N`, if the two homomorphisms are equal when coerced to their underlying functions (i.e., `⇑f = ⇑g`), then the original two homomorphisms themselves are equal (`f = g`). This essentially asserts the injectivity of the coercion from an additive monoid homomorphism to its underlying function. However, it's deprecated and it is recommended to use `DFunLike.coe_injective` instead.
More concisely: Given additive monoid homomorphisms `f` and `g` from an additive monoid `M` to an additive monoid `N`, if their underlying functions are equal (`⇑f = ⇑g`), then the homomorphisms themselves are equal (`f = g`).
|
MonoidHom.map_exists_right_inv
theorem MonoidHom.map_exists_right_inv :
∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : MulOneClass M] [inst_1 : MulOneClass N]
[inst_2 : FunLike F M N] [inst_3 : MonoidHomClass F M N] (f : F) {x : M}, (∃ y, x * y = 1) → ∃ y, f x * y = 1
The theorem `MonoidHom.map_exists_right_inv` states that given any monoid homomorphism `f` from a monoid `M` to another monoid `N`, and an element `x` from `M`, if `x` has a right inverse (i.e., there exists an element `y` in `M` such that the multiplication of `x` and `y` gives the identity element `1`), then the image of `x` under `f`, denoted as `f x`, also has a right inverse in `N`. This is an important property that enforces the consistent structure preservation of homomorphisms between algebraic structures. The function `f` here is assumed to be part of the class `FunLike F M N` and `MonoidHomClass F M N`, representing it is a function from `M` to `N` and also a monoid homomorphism.
More concisely: If `f` is a monoid homomorphism from monoid `M` to monoid `N` and `x` in `M` has a right inverse, then `f(x)` has a right inverse in `N`.
|
OneHom.congr_arg
theorem OneHom.congr_arg :
∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] (f : OneHom M N) {x y : M}, x = y → f x = f y := by
sorry
This theorem, `OneHom.congr_arg`, establishes the principle of function congruence for `OneHom` type functions in Lean, which are functions preserving the `One` (multiplicative identity) structure. Specifically, if `M` and `N` are types endowed with a `One` structure, `f` is a function from `M` to `N` of type `OneHom`, and `x` and `y` are elements of `M` such that `x` equals `y`, then `f(x)` will equal `f(y)`. In other words, if two inputs to a `OneHom` function are the same, their outputs will also be the same. Please note that this theorem is deprecated and the use of `DFunLike.congr_arg` is recommended instead.
More concisely: If `f` is a function of type `OneHom (M : Type) (N : Type)` and `x = y` in `M`, then `f x = f y` in `N`.
|
map_eq_zero_iff
theorem map_eq_zero_iff :
∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Zero M] [inst_1 : Zero N] [inst_2 : FunLike F M N]
[inst_3 : ZeroHomClass F M N] (f : F), Function.Injective ⇑f → ∀ {x : M}, f x = 0 ↔ x = 0
The theorem `map_eq_zero_iff` states that for any types `M`, `N` and `F`, given that `M` and `N` are equipped with zero elements, `F` is a function-like type from `M` to `N`, and `F` forms a zero homomorphism from `M` to `N`, then for any function `f` of type `F`, if `f` is injective, for any element `x` of type `M`, `f(x)` is equal to the zero element of `N` if and only if `x` is the zero element of `M`. In other words, an injective zero homomorphism only maps the zero element to the zero element.
More concisely: An injective zero homomorphism maps the zero element to the zero element.
|
map_pow
theorem map_pow :
∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : Monoid G] [inst_2 : Monoid H]
[inst_3 : MonoidHomClass F G H] (f : F) (a : G) (n : ℕ), f (a ^ n) = f a ^ n
The theorem `map_pow` states that for any types `G`, `H`, and `F`, where `F` has a structure of `FunLike` (meaning terms of type `F` can be injectively cast into functions from `G` to `H`), `G` and `H` are both monoids and `F` is a monoid homomorphism from `G` to `H`, then for any homomorphism `f` of type `F`, any element `a` from `G` and any natural number `n`, the result of applying `f` to `a` raised to the power `n` is equal to the result of applying `f` to `a`, and then raising that result to the power `n`. In simple words, the homomorphism preserves the power operation.
More concisely: For any monoid homomorphism `f` between monoids `G` and `H`, and for all `a` in `G` and natural number `n`, `f (a ^ n) = (f a) ^ n`.
|
AddMonoidHom.coe_coe
theorem AddMonoidHom.coe_coe :
∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
[inst_2 : FunLike F M N] [inst_3 : AddMonoidHomClass F M N] (f : F), ⇑↑f = ⇑f
This theorem, `AddMonoidHom.coe_coe`, states that for any types `M`, `N`, and `F`, where `M` and `N` have the structure of an `AddZeroClass` (i.e., they are additive monoids with zero), `F` is a function-like object from `M` to `N`, and `F` is an additive monoid homomorphism class, then for any object `f` of type `F`, the double coercion of `f` (first coercing `f` to a function from `M` to `N`, and then treating that function as a function from `M` to `N`) is equal to the single coercion of `f`. In simpler terms, adding an extra layer of coercion to `f` does not change its behavior as a function.
More concisely: Given an additive monoid homomorphism class `F` from an additive monoid `M` to an additive monoid `N`, the double application of the coercion from `F` to a function from `M` to `N` is equal to the single application.
|
ZeroHom.comp_assoc
theorem ZeroHom.comp_assoc :
∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_10} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero P]
[inst_3 : Zero Q] (f : ZeroHom M N) (g : ZeroHom N P) (h : ZeroHom P Q), (h.comp g).comp f = h.comp (g.comp f)
This theorem states that the composition of additive monoid homomorphisms is associative. In other words, given three types `M`, `N`, `P`, and `Q` which all have a zero element (i.e., they are additive monoids), and given three additive monoid homomorphisms `f` from `M` to `N`, `g` from `N` to `P`, and `h` from `P` to `Q`, the composition of `h` and `g`, when further composed with `f`, is the same as the composition of `h` with the composition of `g` and `f`. This essentially means that the parentheses don't matter when you're composing these homomorphisms – `(h.comp g).comp f` and `h.comp (g.comp f)` will give the same result.
More concisely: Given three additive monoid homomorphisms `f : M -> N`, `g : N -> P`, and `h : P -> Q` between additive monoids `M`, `N`, `P`, and `Q`, the associativity of homomorphism composition holds, that is, `(h . g) . f = h . (g . f)`.
|
map_neg
theorem map_neg :
∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : AddGroup G]
[inst_2 : SubtractionMonoid H] [inst_3 : AddMonoidHomClass F G H] (f : F) (a : G), f (-a) = -f a
This theorem states that homomorphisms of additive groups preserve negation. In more detail, for any types `G`, `H`, and `F`, if `F` is a function-like structure that maps elements from `G` to `H`, `G` is an additive group, `H` is a subtraction monoid, and `F` is an additive monoid homomorphism class from `G` to `H`, then for any element `a` of `G` and any function `f` of type `F`, applying `f` to the negation of `a` gives the same result as negating the result of applying `f` to `a`. Mathematically, this can be expressed as: for all `a` in `G`, `f(-a) = -f(a)`. This preservation of negation is a key property of group homomorphisms.
More concisely: Given an additive group `G`, an additive monoid `H`, and an additive monoid homomorphism `F` from `G` to `H`, for all elements `a` in `G`, `F(-a) = -F(a)`.
|
AddMonoidHom.map_exists_left_neg
theorem AddMonoidHom.map_exists_left_neg :
∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
[inst_2 : FunLike F M N] [inst_3 : AddMonoidHomClass F M N] (f : F) {x : M},
(∃ y, y + x = 0) → ∃ y, y + f x = 0
This theorem states that, given an additive monoid homomorphism `f` from `M` to `N` and an element `x` in `M`, if there exists an element `y` in `M` such that `y + x = 0` (i.e., `x` has a left additive inverse), then there also exists an element `y` in `N` such that `y + f(x) = 0` (i.e., `f(x)` has a left additive inverse in `N`). The homomorphism `f` is a term of type `F`, which is a function-like object from `M` to `N`. The typeclasses `AddZeroClass M` and `AddZeroClass N` signify that `M` and `N` are types with addition and a zero element, and `AddMonoidHomClass F M N` asserts that `F` is a class of additive monoid homomorphisms from `M` to `N`.
More concisely: If `f` is an additive monoid homomorphism from an additive monoid `M` with zero element to an additive monoid `N` with zero element, and `x` is an element of `M` with a left additive inverse, then `f(x)` has a left additive inverse in `N`.
|
AddMonoidHom.map_neg
theorem AddMonoidHom.map_neg :
∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : SubtractionMonoid β] (f : α →+ β) (a : α),
f (-a) = -f a
This theorem states that additive group homomorphisms preserve negation. Specifically, for any elements of types `α` and `β`, where `α` is an additive group and `β` is a subtraction monoid, if a function `f` is an additive monoid homomorphism from `α` to `β`, then the homomorphism of the negation of any element `a` in `α` is equal to the negation of the homomorphism of `a`. In simple terms, applying the homomorphism first and then negating is the same as negating first and then applying the homomorphism.
More concisely: For any additive group homomorphism from an additive group to a subtraction monoid, negation is preserved: i.e., -(f(a)) = f(-a).
|
OneHom.ext
theorem OneHom.ext :
∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] ⦃f g : OneHom M N⦄,
(∀ (x : M), f x = g x) → f = g
This theorem states that for any two types `M` and `N` that have a `One` instance (i.e., they have an identity element with respect to a multiplication-like operation), given any two homomorphisms from `M` to `N` (`OneHom M N`), if for every element `x` of type `M`, the result of applying the homomorphisms `f` and `g` to `x` are equal, then the homomorphisms `f` and `g` themselves are equal. This is essentially a statement of function extensionality for homomorphisms between types with a designated "one" element.
More concisely: If `M` and `N` are types with `One` instances, and `f` and `g` are homomorphisms from `M` to `N` such that `f x = g x` for all `x` in `M`, then `f = g`.
|
map_zpow
theorem map_zpow :
∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : Group G] [inst_2 : DivisionMonoid H]
[inst_3 : MonoidHomClass F G H] (f : F) (g : G) (n : ℤ), f (g ^ n) = f g ^ n
The theorem `map_zpow` states that for any types `G`, `H`, and `F`, where `F` is a function-like type from `G` to `H`, `G` is a group, `H` is a division monoid, and `F` forms a monoid homomorphism from `G` to `H`, for any function `f` of type `F`, any element `g` of `G`, and any integer `n`, applying `f` to the integer power of `g` (`g ^ n`) is the same as the integer power of the result of applying `f` to `g` (`f g ^ n`). This theorem essentially states that group homomorphisms preserve integer power.
More concisely: For any group homomorphism f : G -> H between groups G and H with values in a division monoid H, for all g in G and integer n, we have f (g^n) = (f g)^n.
|
map_mul
theorem map_mul :
∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
[inst_3 : MulHomClass F M N] (f : F) (x y : M), f (x * y) = f x * f y
The theorem `map_mul` states that for all types `M`, `N`, and `F`, if `M` and `N` have a multiplication operation, `F` is a type that can be injected into a function from `M` to `N` (denoted by `[FunLike F M N]`), and `F` belongs to the `MulHomClass` (meaning it is a multiplication homomorphism), then for any function `f` of type `F` and any elements `x` and `y` of type `M`, the value of `f` at the product of `x` and `y` is the same as the product of the values of `f` at `x` and `y`. In mathematical terms, this theorem is expressing the property $f(x \cdot y) = f(x) \cdot f(y)$ for a multiplication homomorphism `f`.
More concisely: For any multiplication homomorphism `f` from type `M` to type `N`, `f(x * y) = f(x) * f(y)` for all `x, y` in `M`.
|
map_zero
theorem map_zero :
∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Zero M] [inst_1 : Zero N] [inst_2 : FunLike F M N]
[inst_3 : ZeroHomClass F M N] (f : F), f 0 = 0
The theorem `map_zero` states that for any types `M`, `N`, and `F`, if `M` and `N` have zero elements, `F` is a function-like type from `M` to `N`, and `F` is a zero homomorphism class, then the function `f` of type `F` applied to the zero element of `M` gives the zero element of `N`. Essentially, this theorem states that a zero homomorphism maps the zero element of its domain to the zero element of its codomain.
More concisely: If `F` is a zero homomorphism from the additive group of type `M` to the additive group of type `N` and `0` is the additive identity of `M`, then `F(0)` is the additive identity of `N`.
|
AddMonoidHom.congr_arg
theorem AddMonoidHom.congr_arg :
∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N) {x y : M},
x = y → f x = f y
This theorem states that if two elements `x` and `y` of an additive monoid `M` are equal, then their images under any additive monoid homomorphism `f` from `M` to another additive monoid `N` are also equal. In other words, an additive monoid homomorphism preserves equality of elements. Please note that this theorem has been deprecated and `DFunLike.congr_arg` should be used instead.
More concisely: If `f` is an additive monoid homomorphism between additive monoids `M` and `N`, and `x = y` in `M`, then `f x = f y` in `N`.
|
AddMonoidHom.comp_apply
theorem AddMonoidHom.comp_apply :
∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
[inst_2 : AddZeroClass P] (g : N →+ P) (f : M →+ N) (x : M), (g.comp f) x = g (f x)
The theorem `AddMonoidHom.comp_apply` states that for any types `M`, `N`, and `P` that are instances of an additive monoid (i.e., they have a zero and an addition operation), given an additive monoid homomorphism `g` from `N` to `P` and another additive monoid homomorphism `f` from `M` to `N`, and for any element `x` in `M`, the composition of `g` and `f`, when applied to `x`, is the same as applying `g` to the result of `f` applied to `x`. In mathematical terms, this is saying that (g ∘ f)(x) = g(f(x)), which is the definition of function composition.
More concisely: For any additive monoids M, N, and P, and additive monoid homomorphisms f : M -> N and g : N -> P, (g ∘ f)(x) = g(fx) for all x in M.
|
AddHomClass.map_add
theorem AddHomClass.map_add :
∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} [inst : Add M] [inst_1 : Add N]
[inst_2 : FunLike F M N] [self : AddHomClass F M N] (f : F) (x y : M), f (x + y) = f x + f y
The theorem `AddHomClass.map_add` states that for any types `F`, `M`, and `N`, where `M` and `N` are equipped with addition operations (`Add M` and `Add N` respectively), and `F` is a function-like object from `M` to `N` (expressed by the `FunLike F M N` instance), if `F` is also equipped with an instance of the `AddHomClass F M N` typeclass (which expresses the notion that `F` preserves addition), then for any function `f` of type `F` and any elements `x` and `y` of type `M`, the function `f` preserves the addition operation: the image of the sum `x + y` under `f` is equal to the sum of the images of `x` and `y` under `f`, or mathematically, `f(x + y) = f(x) + f(y)`.
More concisely: For any function-like object `F` from type `M` to `N` with addition preserving instance `AddHomClass F M N`, and for any elements `x` and `y` in `M`, the function `F` satisfies `F(x + y) = F(x) + F(y)`.
|
ZeroHom.map_zero'
theorem ZeroHom.map_zero' :
∀ {M : Type u_10} {N : Type u_11} [inst : Zero M] [inst_1 : Zero N] (self : ZeroHom M N), self.toFun 0 = 0 := by
sorry
This theorem, named `ZeroHom.map_zero'`, states that for any two types `M` and `N` that have a zero (as indicated by the presence of a `Zero` instance for both), any `ZeroHom` function (a function preserving the zero element) from `M` to `N` will map the zero of `M` to the zero of `N`. In other words, the function `self.toFun` when applied to `0` gives `0`.
More concisely: For any types `M` and `N` with zero elements, and any `ZeroHom` function from `M` to `N`, the application of the function to the zero of `M` yields the zero of `N`.
|
MonoidHom.map_inv
theorem MonoidHom.map_inv :
∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : DivisionMonoid β] (f : α →* β) (a : α),
f a⁻¹ = (f a)⁻¹
This theorem states that for any group homomorphism `f` from a group `α` to a division monoid `β`, the inverse of any element `a` in `α` under the homomorphism `f` is the same as the inverse of the image of `a` under `f` in `β`. In other words, group homomorphisms preserve the property of inverses.
More concisely: For any group homomorphism `f` from group `α` to a division monoid `β`, `f(a)^-1 = (f(a))^-1` for all inverses `a^-1, (f(a))^-1` in `α` and `β` respectively.
|
AddMonoidHom.comp_assoc
theorem AddMonoidHom.comp_assoc :
∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_10} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
[inst_2 : AddZeroClass P] [inst_3 : AddZeroClass Q] (f : M →+ N) (g : N →+ P) (h : P →+ Q),
(h.comp g).comp f = h.comp (g.comp f)
The theorem `AddMonoidHom.comp_assoc` states that for any four types `M`, `N`, `P`, `Q` that form additive monoids (meaning they have a zero and a binary add operation), if `f` is an additive monoid homomorphism from `M` to `N`, `g` is an additive monoid homomorphism from `N` to `P`, and `h` is an additive monoid homomorphism from `P` to `Q`, then the composition of morphisms is associative. That is, composing `h` and `g` first and then `f` (i.e., `(h ∘ g) ∘ f`) is the same as composing `h` with the composition of `g` and `f` (i.e., `h ∘ (g ∘ f)`). This is the category-theoretic notion of associativity applied to additive monoid homomorphisms.
More concisely: For any additive monoid homomorphisms `f : M → N`, `g : N → P`, and `h : P → Q` between additive monoids `M`, `N`, `P`, and `Q`, the composition `h ∘ (g ∘ f)` is equal to `(h ∘ g) ∘ f`.
|
MonoidHom.map_zpow
theorem MonoidHom.map_zpow :
∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : DivisionMonoid β] (f : α →* β) (g : α) (n : ℤ),
f (g ^ n) = f g ^ n
The theorem `MonoidHom.map_zpow` states that for any group homomorphism `f` from a group `α` to a division monoid `β`, and any element `g` in `α` and any integer `n`, the mapping of the `n`-th power of `g` under `f` is the same as the `n`-th power of the mapping of `g` under `f`. In other words, the power operation for `g` in the domain group `α` is preserved under the homomorphism `f` when mapped to the codomain `β`.
More concisely: For any group homomorphism from a group to a division monoid and any group element and integer, the image of the element's `n`-th power under the homomorphism is equal to the `n`-th power of the image of the element.
|
map_add_eq_zero
theorem map_add_eq_zero :
∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
[inst_2 : FunLike F M N] [inst_3 : AddMonoidHomClass F M N] (f : F) {a b : M}, a + b = 0 → f a + f b = 0
The theorem `map_add_eq_zero` says that for any types `M`, `N`, and `F`, given that `M` and `N` are both `AddZeroClass` (i.e., they have addition and a zero element), `F` is a function type from `M` to `N` (`FunLike F M N`), and `F` is also an additive monoid homomorphism (`AddMonoidHomClass F M N`), then for any function `f : F` and any elements `a` and `b` of type `M`, if the sum of `a` and `b` equals zero (`a + b = 0`), then the sum of the images of `a` and `b` under `f` also equals zero (`f a + f b = 0`). Essentially, this theorem states that the zero sum property is preserved under the function `f`.
More concisely: Given `AddZeroClass` types `M` and `N`, a function `F : M -> N` being an additive monoid homomorphism implies that `f (a + b) = f a + f b` for all `a, b : M` with `a + b = 0`.
|
AddMonoidHom.map_exists_right_neg
theorem AddMonoidHom.map_exists_right_neg :
∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
[inst_2 : FunLike F M N] [inst_3 : AddMonoidHomClass F M N] (f : F) {x : M},
(∃ y, x + y = 0) → ∃ y, f x + y = 0
The theorem `AddMonoidHom.map_exists_right_neg` states that for any types `M`, `N`, and `F`, where `M` and `N` are additive monoids and `F` is a function-like from `M` to `N` that respects the additive monoid structure (i.e., `F` is an additive monoid homomorphism), if there exists an element `y` in `M` such that `x + y` equals the additive identity `0`, then there also exists an element `y` in `N` such that `f x + y` equals `0`. In simpler terms, if some element `x` of the additive monoid `M` has a right inverse, the image of `x` under the homomorphism `f` has a right inverse in the additive monoid `N` as well.
More concisely: If `F : M -> N` is an additive monoid homomorphism between additive monoids `M` and `N`, and there exists an element `y` in `M` such that `x + y = 0` (left inverse of `x`), then there exists an element `y'` in `N` such that `F x + y' = 0` (left inverse of `F x`).
|
MonoidHom.map_mul
theorem MonoidHom.map_mul :
∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N) (a b : M),
f (a * b) = f a * f b
This theorem states that if `f` is a monoid homomorphism, then the multiplication operation is preserved under `f`. More specifically, for any two elements `a` and `b` from a type `M` that has a multiplication and identity element (a MulOneClass), their multiplication `a * b` mapped by `f` is equal to the multiplication of `f a` and `f b` in another type `N` that also has a multiplication and identity element. This respects one of the key properties of a monoid homomorphism.
More concisely: If `f` is a monoid homomorphism from a monoid `(M, *_1, id_1)` to another monoid `(N, *_2, id_2)`, then for all `a, b` in `M`, `f(a *_1 b) = f(a) *_2 f(b)`.
|
MonoidHom.congr_arg
theorem MonoidHom.congr_arg :
∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N) {x y : M},
x = y → f x = f y
This theorem, `MonoidHom.congr_arg`, states that for any two types `M` and `N`, both of which are instances of the `MulOneClass` (a class representing structures with a multiplication operation and a multiplicative identity), and a monoid homomorphism `f` from `M` to `N`, if two elements `x` and `y` of `M` are equal, then their images under `f` are also equal. Note however that this theorem is deprecated, and it's recommended to use `DFunLike.congr_arg` instead.
More concisely: If `f` is a monoid homomorphism from a MulOneClass type `M` to a MulOneClass type `N`, then for all `x` and `y` in `M` with `x = y`, it follows that `f x = f y`.
|
AddHom.congr_fun
theorem AddHom.congr_fun :
∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] {f g : AddHom M N}, f = g → ∀ (x : M), f x = g x
This theorem, `AddHom.congr_fun`, states that for any two additive homomorphisms `f` and `g` from a type `M` to a type `N` (both types equipped with an addition operation), if `f` is equal to `g`, then the function values of `f` and `g` at any element `x` of `M` are also equal. In other words, if two additive homomorphisms are equal, they return the same output when applied to the same input. This theorem has been deprecated and `DFunLike.congr_fun` should be used instead.
More concisely: If `f` and `g` are equal additive homomorphisms from type `M` to type `N`, then for all `x` in `M`, `f x = g x`.
|
ZeroHomClass.map_zero
theorem ZeroHomClass.map_zero :
∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} [inst : Zero M] [inst_1 : Zero N]
[inst_2 : FunLike F M N] [self : ZeroHomClass F M N] (f : F), f 0 = 0
The theorem `ZeroHomClass.map_zero` states that for any types `F`, `M`, and `N`, when `M` and `N` are types with a zero element (i.e., they are instances of the `Zero` typeclass), `F` is function-like from `M` to `N`, and `F` is an instance of `ZeroHomClass` (a class of functions preserving zero), then for any function `f` of type `F`, the image of `0` under `f` is `0`. In simpler terms, this theorem expresses that a zero-preserving function, when applied to zero, gives zero.
More concisely: For any function `f` of type `F` between types `M` and `N` with zero elements, if `F` is zero-preserving (an instance of `ZeroHomClass`) then `f(0) = 0`.
|
ZeroHom.congr_fun
theorem ZeroHom.congr_fun :
∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] {f g : ZeroHom M N},
f = g → ∀ (x : M), f x = g x
This theorem, `ZeroHom.congr_fun`, which is now deprecated and replaced by `DFunLike.congr_fun`, states that for any two zero-preserving functions `f` and `g` from a type `M` with a zero element to a type `N` with a zero element, if `f` and `g` are equal, then they have the same value at any element `x` of type `M`. In other words, equal zero-preserving functions produce equal results for the same input.
More concisely: If `f` and `g` are zero-preserving functions from a type `M` with zero to a type `N` with zero, then `f x = g x` for all `x` in `M` whenever `f` and `g` are equal.
|
MulHom.ext
theorem MulHom.ext :
∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] ⦃f g : M →ₙ* N⦄, (∀ (x : M), f x = g x) → f = g
This theorem states that for any two multiplication-preserving functions `f` and `g` from a type `M` to a type `N`, both equipped with multiplication structures, if `f` and `g` are identical for all elements of `M`, then `f` and `g` are indeed the same function. In other words, two multiplication-preserving functions between two types with multiplication are the same if they agree on all inputs.
More concisely: If two multiplication-preserving functions from a type with multiplication to another type with multiplication are equal on all elements, then they are equal as functions.
|
Subsingleton.of_oneHomClass
theorem Subsingleton.of_oneHomClass :
∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : One M] [inst_1 : One N] [inst_2 : FunLike F M N]
[inst_3 : Subsingleton M] [inst : OneHomClass F M N], Subsingleton F
The theorem `Subsingleton.of_oneHomClass` states that for all types `M`, `N`, and `F`, if `M` is a subsingleton type (i.e., it has at most one element), `M` and `N` have an identity element (`One M` and `One N`), `F` injectively maps `M` to `N` (`FunLike F M N`), and `F` is a homomorphism that preserves the identity element (`OneHomClass F M N`), then `F` is also a subsingleton type. In other words, if `M` has at most one element and `F` is a structure-preserving map from `M` to `N`, then there is at most one such map `F`.
More concisely: If `M` is a subsingleton type with at most one element, `F` is a function from `M` to another type `N` that is injective, preserves identity elements, and is a homomorphism, then `N` is also a subsingleton type with at most one element.
|
map_sub
theorem map_sub :
∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : AddGroup G]
[inst_2 : SubtractionMonoid H] [inst_3 : AddMonoidHomClass F G H] (f : F) (a b : G), f (a - b) = f a - f b
The theorem `map_sub` states that for any types `G`, `H`, and `F` where `F` is a function-like object from `G` to `H`, `G` is an additive group, `H` is a subtraction monoid, and `F` is a homomorphism class from an additive group `G` to a monoid `H`, then for any function `f` of type `F` and any elements `a` and `b` of `G`, the difference of `a` and `b` under `f` is equal to the difference of `f(a)` and `f(b)`. In other words, an additive group homomorphism preserves the operation of subtraction.
More concisely: For any additive group homomorphism F from group G to monoid H and any elements a, b in G, we have F(a - b) = F(a) - F(b).
|
AddMonoidHom.map_add_neg
theorem AddMonoidHom.map_add_neg :
∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : SubtractionMonoid β] (f : α →+ β) (g h : α),
f (g + -h) = f g + -f h
This theorem states that additive group homomorphisms preserve the subtraction operation. In other words, for any types `α` and `β`, where `α` is an additive group and `β` is a subtraction monoid, and for any additive monoid homomorphism `f` from `α` to `β`, and for any two elements `g` and `h` of `α`, applying `f` to the result of adding `-h` to `g` (`f (g + -h)`) is the same as adding `-f h` to `f g` (`f g + -f h`). This theorem is a formalization of the abstract algebra concept that homomorphisms preserve operations.
More concisely: For any additive monoid homomorphism between additive groups, applying the homomorphism to the difference of two elements is equivalent to subtracting the image of one element from the image of the other.
|
MonoidHom.comp_apply
theorem MonoidHom.comp_apply :
∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : MulOneClass M] [inst_1 : MulOneClass N]
[inst_2 : MulOneClass P] (g : N →* P) (f : M →* N) (x : M), (g.comp f) x = g (f x)
The theorem `MonoidHom.comp_apply` states that for any given types `M`, `N`, and `P`, which are instances of the class `MulOneClass`, and given two monoid homomorphisms `g : N →* P` and `f : M →* N`, the application of the composition of `g` and `f` to an element `x` of `M` is equal to the application of `g` to the result of applying `f` to `x`. In other words, `(MonoidHom.comp g f) x = g (f x)`. This theorem formalizes the concept of function composition in the context of monoid homomorphisms.
More concisely: For any types `M`, `N`, and `P` instanced with `MulOneClass`, and given monoid homomorphisms `f : M →* N` and `g : N →* P`, `(MonoidHom.comp g f) x = g (f x)` for all `x : M`.
|
map_add_neg
theorem map_add_neg :
∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : AddGroup G]
[inst_2 : SubtractionMonoid H] [inst_3 : AddMonoidHomClass F G H] (f : F) (a b : G), f (a + -b) = f a + -f b
This theorem states that all additive group homomorphisms preserve subtraction. More specifically, for any types `G`, `H`, and `F`, if `F` can be viewed as a function from `G` to `H`, `G` has the structure of an additive group, `H` has the structure of a subtraction monoid, and `F` conforms to class `AddMonoidHomClass` (i.e., it behaves like a homomorphism between additive monoids), then for any such function `f` and any elements `a` and `b` of `G`, applying `f` to the result of adding the additive inverse of `b` to `a` is the same as subtracting `f` applied to `b` from `f` applied to `a`. In mathematical terms, it states that for all `a` and `b` in `G`, `f(a + -b) = f(a) + -f(b)`.
More concisely: For any additive group homomorphism `f` from type `G` to type `H` with `H` being a subtraction monoid, `f(a + (-b)) = f(a) + (-f(b))` for all `a, b` in `G`.
|
map_mul_eq_one
theorem map_mul_eq_one :
∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : MulOneClass M] [inst_1 : MulOneClass N]
[inst_2 : FunLike F M N] [inst_3 : MonoidHomClass F M N] (f : F) {a b : M}, a * b = 1 → f a * f b = 1
The theorem `map_mul_eq_one` states that for any types `M`, `N`, and `F`, such that `M` and `N` are both mul-one classes (i.e., they are equipped with multiplication and have a specified "one" element), `F` is a class of functions from `M` to `N` (i.e., is `FunLike`), and `F` is a monoid homomorphism class from `M` to `N`, then for any function `f` of type `F` and any elements `a` and `b` of `M`, if the product of `a` and `b` equals `1`, then the product of `f(a)` and `f(b)` also equals `1`. In mathematical terms, this theorem states that a monoid homomorphism preserves the identity element under multiplication.
More concisely: A monoid homomorphism preserves the identity element under multiplication, i.e., for any monoids (M, ¹M) and (N, ¹N), and a monoid homomorphism f : M -> N, if a * b = ¹M, then f(a) * f(b) = ¹N.
|
ZeroHom.ext_iff
theorem ZeroHom.ext_iff :
∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] {f g : ZeroHom M N},
f = g ↔ ∀ (x : M), f x = g x
This theorem, `ZeroHom.ext_iff`, states that for any two zero morphisms `f` and `g` from a type `M` to another type `N` where both `M` and `N` are equipped with a zero element, `f` is equal to `g` if and only if `f x` equals `g x` for all `x` in `M`. This is a fundamental property of function equality, stating that two functions are equal if they produce the same output for every input. Note, however, that this theorem is deprecated and `DFunLike.ext_iff` should be used instead.
More concisely: For zero morphisms `f` and `g` from types `M` with zero elements, `f` equals `g` if and only if `f x = g x` for all `x` in `M`.
|
AddHom.ext_iff
theorem AddHom.ext_iff :
∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] {f g : AddHom M N}, f = g ↔ ∀ (x : M), f x = g x
This theorem, which is now deprecated and recommends using `DFunLike.ext_iff` instead, states that for any two additive homomorphisms `f` and `g` from an additive type `M` to another additive type `N`, `f` is equal to `g` if and only if `f` and `g` have the same result when applied to any element `x` from `M`. Here, `AddHom M N` denotes an additive homomorphism from `M` to `N`, and `Add M` and `Add N` indicate that `M` and `N` are types with an addition operation.
More concisely: For any additive types M and N and additive homomorphisms f and g from M to N, f = g if and only if f(x) = g(x) for all x in M.
|
AddMonoidHom.map_sub
theorem AddMonoidHom.map_sub :
∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : SubtractionMonoid β] (f : α →+ β) (g h : α),
f (g - h) = f g - f h
The theorem `AddMonoidHom.map_sub` states that for any given additive group homomorphism `f` from a type `α` to a type `β`, both of which have subtraction structures, the homomorphism will preserve the subtraction operation. This means that applying the homomorphism `f` to the result of subtracting `h` from `g` (where `g` and `h` are elements of type `α`) will yield the same result as subtracting the image of `h` under `f` from the image of `g` under `f` in type `β`. In mathematical terms, this can be written as `f(g - h) = f(g) - f(h)`.
More concisely: Given an additive group homomorphism \(f : \alpha \to \beta\) between additive groups, \(f(g - h) = f(g) - f(h)\) for all \(g, h \in \alpha\).
|