IsUnit.map
theorem IsUnit.map :
∀ {F : Type u_1} {M : Type u_4} {N : Type u_5} [inst : FunLike F M N] [inst_1 : Monoid M] [inst_2 : Monoid N]
[inst_3 : MonoidHomClass F M N] (f : F) {x : M}, IsUnit x → IsUnit (f x)
This theorem states that for any two types `M` and `N` that have `Monoid` structures, and any type `F` that can be treated as a function from `M` to `N` and also satisfies the `MonoidHomClass` typeclass, if an element `x` of `M` is a unit (meaning it has a two-sided inverse in its monoid structure), then the image of `x` under any function `f` of type `F` is also a unit in `N`. Essentially, it states that the property of being a unit is preserved under homomorphisms between monoids.
More concisely: If `M` and `N` are monoids, `F: M → N` is a monoid homomorphism, and `x` is a unit in `M`, then `F(x)` is a unit in `N`.
|
Units.map_id
theorem Units.map_id : ∀ (M : Type u) [inst : Monoid M], Units.map (MonoidHom.id M) = MonoidHom.id Mˣ
The theorem `Units.map_id` states that for all types `M` equipped with a monoid structure, the homomorphism induced on units by the identity map on `M` is itself the identity map on the group of units of `M`. In other words, mapping each unit of a monoid `M` via the identity function results in the identity map on the units of `M`. This theorem shows the compatibility of unit mapping and identity mapping in the context of monoids.
More concisely: For all monoids M, the identity map on M preserves the identity element when restricted to the group of units of M.
|
IsUnit.eq_on_inv
theorem IsUnit.eq_on_inv :
∀ {F : Type u_1} {G : Type u_2} {N : Type u_3} [inst : DivisionMonoid G] [inst_1 : Monoid N]
[inst_2 : FunLike F G N] [inst_3 : MonoidHomClass F G N] {x : G},
IsUnit x → ∀ (f g : F), f x = g x → f x⁻¹ = g x⁻¹
This theorem states that given two homomorphisms from a division monoid to a monoid, if they are identical at a unit element `x`, then they will also be identical at the inverse of `x`. Here, a division monoid is a structure with an operation that combines two elements to give a third and has a multiplicative identity, an inverse for each element, and the operation is associative. A monoid is similar but doesn't necessarily have inverses for each element. A homomorphism is a map between two algebraic structures that preserves the operations of the structures. The concept of a unit refers to an element that has a two-sided inverse.
More concisely: If two homomorphisms from a division monoid to a monoid agree at a unit element and its inverse, then they are equal.
|
eq_on_inv
theorem eq_on_inv :
∀ {F : Type u_1} {G : Type u_2} {M : Type u_3} [inst : Group G] [inst_1 : Monoid M] [inst_2 : FunLike F G M]
[inst_3 : MonoidHomClass F G M] (f g : F) {x : G}, f x = g x → f x⁻¹ = g x⁻¹
The theorem `eq_on_inv` states that for any two function-like objects `f` and `g` of type `F` that act as homomorphisms from a group `G` to a monoid `M`, if `f` and `g` are equal at a certain element `x` of the group, then they are also equal at the inverse of `x` (`x⁻¹`). This theorem leverages the structures of the group and the monoid as well as the properties of the homomorphisms to establish this equality.
More concisely: If `f` and `g` are homomorphisms from a group `G` to a monoid `M` such that `f(x) = g(x)` for some `x` in `G`, then `f(x⁻¹) = g(x⁻¹)`.
|
IsAddUnit.map
theorem IsAddUnit.map :
∀ {F : Type u_1} {M : Type u_4} {N : Type u_5} [inst : FunLike F M N] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N]
[inst_3 : AddMonoidHomClass F M N] (f : F) {x : M}, IsAddUnit x → IsAddUnit (f x)
The theorem `IsAddUnit.map` states that for any types `F`, `M`, and `N`, if `F` is a function-like object mapping from `M` to `N`, `M` and `N` are both addmonoids, and `F` is a homomorphism between these addmonoids, then for any function `f` of type `F` and any element `x` of type `M`, if `x` is an additive unit in `M` (i.e., it has a two-sided additive inverse), the image of `x` under `f` is also an additive unit in `N`. In other words, homomorphisms preserve the property of being an additive unit.
More concisely: If `F` is a homomorphism between addmonoids `M` and `N`, and `x` is an additive unit in `M`, then `F(x)` is an additive unit in `N`.
|
eq_on_neg
theorem eq_on_neg :
∀ {F : Type u_1} {G : Type u_2} {M : Type u_3} [inst : AddGroup G] [inst_1 : AddMonoid M] [inst_2 : FunLike F G M]
[inst_3 : AddMonoidHomClass F G M] (f g : F) {x : G}, f x = g x → f (-x) = g (-x)
This theorem states that if two homomorphisms from an additive group to an additive monoid agree on an element `x`, then they also agree on the negation of `x`. More formally, given any additive group `G`, any additive monoid `M`, any type `F` that has a `FunLike` instance from `G` to `M`, a class instance of `AddMonoidHomClass` for `F`, `G`, and `M`, and two homomorphisms `f` and `g` of type `F`, if `f` and `g` are equal at some element `x` from `G`, then `f` applied to `-x` is equal to `g` applied to `-x`. This is a property of the negation in the additive group and the preservation of the group structure by the homomorphisms.
More concisely: If two additive group homomorphisms agree on an element and its negation, then they are equal everywhere.
|
Units.coe_map
theorem Units.coe_map :
∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N) (x : Mˣ),
↑((Units.map f) x) = f ↑x
The theorem `Units.coe_map` states that for any two types `M` and `N` which are instances of the `Monoid` class, and for any monoid homomorphism `f` from `M` to `N`, and any unit `x` in `M`, applying the unit map induced by `f` to `x` and then taking the corresponding element in `N` (i.e., `↑((Units.map f) x)`) is the same as first taking the corresponding element of `x` in `M` and then applying `f` (i.e., `f ↑x`). In other words, the process of mapping units commutes with the process of taking corresponding elements in their respective monoids.
More concisely: For any monoid homomorphism f between monoids M and N and any unit x in M, the application of the unit map and f commutes: ↑((Units.map f) x) = f ↑x.
|
IsAddUnit.eq_on_neg
theorem IsAddUnit.eq_on_neg :
∀ {F : Type u_1} {G : Type u_2} {N : Type u_3} [inst : SubtractionMonoid G] [inst_1 : AddMonoid N]
[inst_2 : FunLike F G N] [inst_3 : AddMonoidHomClass F G N] {x : G},
IsAddUnit x → ∀ (f g : F), f x = g x → f (-x) = g (-x)
The theorem `IsAddUnit.eq_on_neg` states that for all types `F`, `G`, and `N`, where `G` is a subtraction monoid, `N` is an additive monoid, `F` is a function-like structure from `G` to `N`, and `F` forms an additive monoid homomorphism from `G` to `N`, if two homomorphisms `f` and `g` from `G` to `N` are equal at an additive unit `x` in `G`, then they are also equal at the negation of `x`.
More concisely: If `f` and `g` are additive monoid homomorphisms from a subtraction monoid `G` to an additive monoid `N`, and `f(x) = g(x)` for some additive unit `x` in `G`, then `f(-x) = g(-x)`.
|