LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.GroupTheory.Subgroup.Basic

`Subgroup.comap_mono` theorem Subgroup.comap_mono : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {K K' : Subgroup N}, K ≤ K' → Subgroup.comap f K ≤ Subgroup.comap f K' The theorem `Subgroup.comap_mono` states that for any two subgroups `K` and `K'` of a group `N` and a monoid homomorphism `f` from a group `G` to `N`, if `K` is a subset of `K'` (expressed as `K ≤ K'`), then the preimage of `K` under `f` is a subset of the preimage of `K'` under `f` (expressed as `Subgroup.comap f K ≤ Subgroup.comap f K'`). In other words, if we map `G` to `N` using `f`, and `K` is contained in `K'` in `N`, then the elements of `G` that map to `K` are contained within the elements of `G` that map to `K'`. More concisely: If `f` is a monoid homomorphism from a group `G` to a group `N`, `K` is a subgroup of `K'` in `N`, then the preimage of `K` under `f` is a subgroup of the preimage of `K'` under `f` in `G`.
`AddSubgroup.map_sup` theorem AddSubgroup.map_sup : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H K : AddSubgroup G) (f : G →+ N), AddSubgroup.map f (H ⊔ K) = AddSubgroup.map f H ⊔ AddSubgroup.map f K The theorem `AddSubgroup.map_sup` states that for any two additively-structured subgroups `H` and `K` within a type `G` that forms an additive group, and a homomorphism `f` from `G` to another additive group `N`, the image of the additive subgroup resulting from the join (or superset) of `H` and `K` under the action of `f`, is equal to the join (or superset) of the respective images of `H` and `K` under the action of `f`. In other words, the image of the union of two additive subgroups under an additive monoid homomorphism is the same as the union of the images of the individual subgroups. This theorem is talking about the distributive property of the map function over the join operation in the context of additive subgroups and additive monoid homomorphisms. More concisely: For any additive subgroups H and K of an additive group G and any additive monoid homomorphism f from G to an additive group N, the image of H ∪ K under f is equal to the image of H under f ∪ the image of K under f.
`AddSubgroup.le_comap_map` theorem AddSubgroup.le_comap_map : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (H : AddSubgroup G), H ≤ AddSubgroup.comap f (AddSubgroup.map f H) The theorem `AddSubgroup.le_comap_map` states that for any additive group homomorphism `f` from an additive group `G` to another additive group `N`, and any additive subgroup `H` of `G`, `H` is a subset of the preimage under `f` of the image under `f` of `H`. In other words, every element of the subgroup `H` is mapped to an element in `N` and then mapped back to an element in `G` that is in `H`. This theorem is a form of the fundamental property of the image and preimage (or inverse image) under a function. More concisely: For any additive group homomorphism f from an additive group G to another additive group N and any additive subgroup H of G, the image of H under f is a subset of the preimage of the image of H under f.
`Subgroup.subtype_injective` theorem Subgroup.subtype_injective : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), Function.Injective ⇑H.subtype The theorem `Subgroup.subtype_injective` states that for any given subgroup `H` of a group `G`, the function produced by `Subgroup.subtype H` is injective. In other words, if we have two elements from the subgroup `H` and they map to the same element in the group `G` under the `Subgroup.subtype H` function, then those two elements must have been the same to begin with. This is a property of the natural group homomorphism from a subgroup of a group to the group itself. More concisely: The function `Subgroup.subtype` from a subgroup `H` of a group `G` to `G` is an injection.
`Subgroup.pow_mem` theorem Subgroup.pow_mem : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) {x : G}, x ∈ K → ∀ (n : ℕ), x ^ n ∈ K This theorem, `Subgroup.pow_mem`, asserts that for any group `G` and any subgroup `K` of `G`, if an element `x` belongs to `K`, then `x` raised to any natural number `n` also belongs to `K`. In other words, any power of an element in a subgroup remains in the subgroup. More concisely: For any group `G` and subgroup `K`, if `x` is an element of `K`, then for all natural numbers `n`, `x^n` is also an element of `K`.
`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.2` theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.2 : ∀ {S : Type u_5} {G : Type u_6} [inst : InvolutiveNeg G] {x : SetLike S G} [inst_1 : NegMemClass S G] {H : S} {x_1 : G}, (-x_1 ∈ H) = (x_1 ∈ H) This theorem states that for any type `S` and `G`, where `G` has an involutive negation operation (i.e., double negation returns the original element), and type `S` is a set-like structure containing elements of type `G`. Moreover, if `S` has an instance of `NegMemClass` (meaning that if an element belongs to a set-like object `S`, its negation also belongs to `S`), then for any set `H` of type `S` and any element `x_1` of type `G`, `x_1` belonging to `H` is equivalent to `-x_1` belonging to `H`. In mathematical terms, for a set `H` and an element `x_1`, `x_1 ∈ H` if and only if `-x_1 ∈ H`. More concisely: For any set-like structure `S` over type `G` with an involutive negation operation and an instance of `NegMemClass`, the membership of an element `x_1` in `S` is equivalent to the membership of its negation `-x_1` in `S`.
`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.39` theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.39 : ∀ {G : Type u_1} [inst : AddGroup G] (x : G), (x ∈ ⊤) = True This theorem is a statement in group theory related to additive groups. It says that for any type `G`, given that `G` forms an additive group `AddGroup G`, any element `x` of `G` is a member of the top subgroup (denoted by `⊤`). In other words, every element of an additive group is included in the universal subgroup. More concisely: In any additive group, every element is contained in the universal subgroup.
`Subgroup.inv_mem_iff` theorem Subgroup.inv_mem_iff : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) {x : G}, x⁻¹ ∈ H ↔ x ∈ H This theorem states that for any group `G` and a subgroup `H` of `G`, an element `x` of `G` is in `H` if and only if the inverse of `x` is in `H`. In other words, a subgroup of a group contains an element `x` if it also contains the inverse of that element `x⁻¹`, and vice versa. This is a property unique to subgroups in the field of group theory in mathematics. More concisely: For any group `G` and subgroup `H`, an element `x` belongs to `H` if and only if its inverse `x⁻¹` belongs to `H`.
`AddSubgroup.coe_eq_univ` theorem AddSubgroup.coe_eq_univ : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, ↑H = Set.univ ↔ H = ⊤ := by sorry This theorem states that for any given type `G` that forms an additive group, and any `H` which is a subgroup of `G`, the coercion of `H` to a set is equal to the universal set if and only if `H` is the top element of the lattice of additive subgroups, i.e., `H` is the whole group `G`. In mathematical terms, this means that an additive subgroup `H` of a group `G` spans the entire group if and only if `H` is equal to `G` itself. More concisely: For an additive group `G` and its subgroup `H`, `coerce H to set = {-} : set G <=> H = G`.
`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.38` theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.38 : ∀ {G : Type u_1} [inst : Group G] (x : G), (x ∈ ⊤) = True This theorem states that for any group `G` and any element `x` of `G`, `x` is an element of the group's top (or universal) subgroup. In the context of group theory, the top subgroup is the group itself. Therefore, this theorem is essentially saying that any element of a group is, by definition, an element of that group. More concisely: For any group `G` and any of its elements `x`, `x` is a member of group `G`.
`Subgroup.coe_mk` theorem Subgroup.coe_mk : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (x : G) (hx : x ∈ H), ↑⟨x, hx⟩ = x := by sorry This theorem, `Subgroup.coe_mk`, states that for any given type `G` that forms a group, any subgroup `H` of `G`, and any element `x` of `G` that belongs to `H`, the coercion of a structure that consists of `x` and the proof of `x` belonging to `H` to `G` is equal to `x` itself. In mathematical terms, this theorem specifies the behavior of the coercion function (denoted by `↑`) from the set of elements in the subgroup `H` to the group `G`. More concisely: For any group `G` and subgroup `H` of `G`, and for any element `x` in `H`, the coercion of `(x, ‹x ∈ H›)` to `G` equals `x`.
`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.19` theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.19 : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) (x : G), (x ∈ K.toAddSubmonoid) = (x ∈ K) This theorem states that for any given additive group `G` and any additive subgroup `K` of `G`, an element `x` of `G` belongs to the additive submonoid generated by `K` if and only if `x` belongs to `K` itself. In other words, in the context of additive groups, the subset of `G` defined by `K` as a subgroup is the same as the subset defined by `K` as a submonoid. More concisely: An additive subgroup of an abelian group equals the additive submonoid generated by it.
`Subgroup.closure_le` theorem Subgroup.closure_le : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) {k : Set G}, Subgroup.closure k ≤ K ↔ k ⊆ ↑K This theorem states that for any group `G` and any subgroup `K` of `G`, the closure of a set `k` (of elements in `G`) is a subset of `K` if and only if `k` is a subset of `K`. In other words, a subgroup `K` includes the `Subgroup.closure` of a set `k` if and only if it includes the set `k` itself. The closure of a set, in this context, represents the smallest subgroup that contains that set. More concisely: A subgroup K of a group G contains the closure of a set k if and only if k is a subset of K.
`AddSubgroup.gc_map_comap` theorem AddSubgroup.gc_map_comap : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N), GaloisConnection (AddSubgroup.map f) (AddSubgroup.comap f) The theorem `AddSubgroup.gc_map_comap` establishes a Galois connection between the functions `AddSubgroup.map f` and `AddSubgroup.comap f` for any additively homomorphic function `f` from an additive group `G` to another additive group `N`. In other words, for any additive subgroup `H` of `G` and `K` of `N`, the image of `H` under the function `f` is a subgroup of `K` if and only if `H` is a subgroup of the preimage of `K` under `f`. More concisely: For any additively homomorphic function `f` between additive groups `G` and `N`, the functions `AddSubgroup.map f` and `AddSubgroup.comap f` define a Galois connection between the subgroups of `G` and `N`.
`MonoidHom.map_range` theorem MonoidHom.map_range : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} {P : Type u_6} [inst_1 : Group N] [inst_2 : Group P] (g : N →* P) (f : G →* N), Subgroup.map g f.range = (g.comp f).range The theorem `MonoidHom.map_range` states that for any two groups `G`, `N` and `P`, and any two monoid homomorphisms `g: N -> P` and `f: G -> N`, the subgroup of `P` obtained by mapping the range of `f` under the homomorphism `g` is equal to the range of the composite homomorphism `g ∘ f`. In other words, applying a monoid homomorphism to the range of another homomorphism is the same as taking the range of the composition of those two homomorphisms. More concisely: For any groups G, N, and P, and monoid homomorphisms f : G -> N and g : N -> P, the image of f under g is equal to the image of the range of f under g.
`Subgroup.map_top_of_surjective` theorem Subgroup.map_top_of_surjective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N), Function.Surjective ⇑f → Subgroup.map f ⊤ = ⊤ The theorem `Subgroup.map_top_of_surjective` states that for every surjective monoid homomorphism `f` from a group `G` to another group `N`, the image of the entire group `G` (denoted by `⊤`) under the map `f` is the entire group `N`. In other words, if every element in group `N` is the image of some element in group `G` under the homomorphism `f`, then every element of `N` is in the image of `G` under `f`. This theorem is a property regarding surjective homomorphisms and subgroup mappings in group theory. More concisely: If `f` is a surjective group homomorphism from `G` to `N`, then `⊤(G) = N`.
`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.76` theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.76 : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} {h : ↥K}, (h ∈ H.subgroupOf K) = (↑h ∈ H) This theorem states that for any type `G` with a group structure and any subgroups `H` and `K` of `G`, if we have an element `h` of subgroup `K`, then `h` is in the subgroup of `H` and `K` (i.e., the intersection of `H` and `K` as viewed as a subgroup of `K`) if and only if the underlying element of `h` in `G` is in `H`. More concisely: For any group `G` and subgroups `H` and `K` of `G`, an element `h` in `K` belongs to the intersection of `H` and `K` as subgroups of `G` if and only if `h` is in `H` as elements of `G`.
`Subgroup.closure_eq` theorem Subgroup.closure_eq : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G), Subgroup.closure ↑K = K This theorem states that for any group `G`, the `Subgroup.closure` of a subgroup `K` of `G` is equal to `K` itself. In other words, when we take the closure of a subgroup (which is the smallest subgroup containing a given set), it remains the same subgroup. This is because a subgroup is already closed under the group operations, so the process of taking the closure doesn't change anything. More concisely: For any subgroup `K` of a group `G`, `Subgroup.closure K` equals `K`.
`AddSubgroup.IsCommutative.is_comm` theorem AddSubgroup.IsCommutative.is_comm : ∀ {A : Type u_4} [inst : AddGroup A] {H : AddSubgroup A}, H.IsCommutative → Std.Commutative fun x x_1 => x + x_1 This theorem states that for any type `A` which is equipped with an addition group structure, and for any additive subgroup `H` of `A`, if `H` is commutative, then the standard addition operation `(+)` on `H` is commutative as well. In other words, for all `x` and `x_1` in `H`, the order in which they are added does not matter, i.e., `x + x_1 = x_1 + x`. More concisely: For any commutative additive subgroup `H` of an additive group `A`, the group operation `(+)` on `H` is commutative.
`Subgroup.Characteristic.fixed` theorem Subgroup.Characteristic.fixed : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.Characteristic → ∀ (ϕ : G ≃* G), Subgroup.comap ϕ.toMonoidHom H = H The theorem `Subgroup.Characteristic.fixed` states that for any group `G` and any subgroup `H` of `G`, if `H` is a characteristic subgroup of `G` (meaning that it is invariant under all automorphisms of `G`), then for any automorphism `ϕ` of `G`, the preimage of `H` under the monoid homomorphism associated with `ϕ` is equal to `H` itself. In other words, characteristic subgroups are preserved under all automorphisms of the group. More concisely: A characteristic subgroup of a group is fixed under any automorphism of the group.
`AddSubgroup.closure_union` theorem AddSubgroup.closure_union : ∀ {G : Type u_1} [inst : AddGroup G] (s t : Set G), AddSubgroup.closure (s ∪ t) = AddSubgroup.closure s ⊔ AddSubgroup.closure t The theorem `AddSubgroup.closure_union` states that for any type `G` that has `AddGroup` instance and for any two sets `s` and `t` of type `G`, the additive subgroup generated by the union of `s` and `t` is equal to the supremum of the additive subgroups generated by `s` and `t` individually. In other words, this theorem is expressing the property that the closure operation of an additive subgroup preserves the union operation. More concisely: The additive subgroup generated by the union of two sets is equal to the sum of their additive subgroups.
`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.37` theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.37 : ∀ {G : Type u_1} [inst : AddGroup G] {x : G}, (x ∈ ⊥) = (x = 0) This theorem states that for any type `G` which is an additive group, and for any element `x` of `G`, `x` belongs to the trivial subgroup if and only if `x` is the additive identity (0) of the group. In mathematical terminology, this theorem asserts that an element belongs to the trivial subgroup of an additive group if and only if that element is the zero element. More concisely: An element of an additive group is in the trivial subgroup if and only if it is the additive identity.
`AddSubgroup.Characteristic.fixed` theorem AddSubgroup.Characteristic.fixed : ∀ {A : Type u_4} [inst : AddGroup A] {H : AddSubgroup A}, H.Characteristic → ∀ (ϕ : A ≃+ A), AddSubgroup.comap ϕ.toAddMonoidHom H = H The theorem `AddSubgroup.Characteristic.fixed` states that for any type `A` with an addition group structure and any subgroup `H` of `A`, if `H` is characteristic, then it is preserved under all automorphisms. In other words, the preimage of `H` under any automorphism `ϕ` is `H` itself. This means `H` is invariant under all automorphisms of the additive group `A`. More concisely: If `A` is an additive group and `H` is a characteristic subgroup of `A`, then any automorphism of `A` maps `H` to itself.
`AddSubgroup.map_mono` theorem AddSubgroup.map_mono : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {K K' : AddSubgroup G}, K ≤ K' → AddSubgroup.map f K ≤ AddSubgroup.map f K' The theorem `AddSubgroup.map_mono` states that for any two additive subgroups `K` and `K'` of an additive group `G` and a given additive monoid homomorphism `f` from `G` to another additive group `N`, if `K` is a subset of `K'` (denoted as `K ≤ K'`), then the image of `K` under `f` is a subset of the image of `K'` under `f`, i.e., `AddSubgroup.map f K ≤ AddSubgroup.map f K'`. This theorem is demonstrating the monotonicity of the map function on additive subgroups. More concisely: If `K ≤ K'` are additive subgroups of an additive group `G` and `f` is an additive monoid homomorphism from `G` to another additive group `N`, then `AddSubgroup.map f K ≤ AddSubgroup.map f K'`.
`NegMemClass.neg_mem` theorem NegMemClass.neg_mem : ∀ {S : Type u_5} {G : Type u_6} [inst : Neg G] [inst_1 : SetLike S G] [self : NegMemClass S G] {s : S} {x : G}, x ∈ s → -x ∈ s This theorem states that for any given set `s` of type `S`, where `S` exhibits the behavior of a set of elements of type `G` (denoted by `SetLike S G`), and `G` has a negation operation, if the set `s` is closed under negation (expressed by `NegMemClass S G`), then if an element `x` of type `G` belongs to the set `s`, the negative of `x` (denoted by `-x`) also belongs to the set `s`. This property is fundamental in the study of mathematical structures that are closed under negation, like additive groups. More concisely: If `S` is a set of type `G` that is closed under negation, then for all `x` in `S`, we have `-x` in `S`.
`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.89` theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.89 : ∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → Group (f i)] (I : Set η) {H : (i : η) → Subgroup (f i)} {p : (i : η) → f i}, (p ∈ Subgroup.pi I H) = ∀ i ∈ I, p i ∈ H i This theorem states that for any given set `I` of indices of type `η`, a family `H` of subgroups each of type `f i`, and a function `p` mapping indices of `I` to elements of the respective `f i`, `p` is a member of the product subgroup `Subgroup.pi I H` if and only if, for each index `i` in `I`, the function `p` evaluated at `i` is a member of the subgroup `H i`. This establishes a condition for membership of an element in the product of a family of subgroups. More concisely: A function `p` belongs to the product subgroup of a family `H` of subgroups indexed by `I` if and only if for all `i` in `I`, `p i` is an element of `H i`.
`AddSubgroup.subtype_range` theorem AddSubgroup.subtype_range : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.subtype.range = H := by sorry The theorem `AddSubgroup.subtype_range` states that for any additive group `G` and any additive subgroup `H` of `G`, the range of the natural group homomorphism from `H` to `G` is precisely `H` itself. This means that applying the subgroup subtype function to every element of `H` will give us exactly the set `H`. In other words, the map that sends each element of `H` to its corresponding element in `G` (defined by the `AddSubgroup.subtype` function) is surjective on `H`. More concisely: The subtype map from an additive subgroup of an additive group to the group itself is a surjection.
`neg_mem_iff` theorem neg_mem_iff : ∀ {S : Type u_5} {G : Type u_6} [inst : InvolutiveNeg G] {x : SetLike S G} [inst_1 : NegMemClass S G] {H : S} {x_1 : G}, -x_1 ∈ H ↔ x_1 ∈ H This theorem states that for any set-like structure `S`, `H`, that is a subset of `G`, where `G` is a type endowed with the property of involutive negation, and any element `x_1` from `G`, the element `x_1` is in `H` if and only if its negation is in `H`. In other words, `H` contains an element and its negation simultaneously. Here, `InvolutiveNeg` refers to the property where the negation of a negation brings you back to the original element (like in the case of numbers), and `NegMemClass` is a class that relates `S` and `G`, suggesting that negation of elements in `S` results in elements in `G`. More concisely: For any set-like structure `S` subset of the involutively negated type `G`, an element `x_1` in `G` belongs to `H` if and only if its negation belongs to `H`.
`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.108` theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.108 : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N}, Function.Injective ⇑f.rangeRestrict = Function.Injective ⇑f The theorem `Mathlib.GroupTheory.Subgroup.Basic._auxLemma.108` states that for any additively-grouped types `G` and `N`, and a function `f` which is an additive monoid homomorphism from `G` to `N`, and any element `y` from `N`, `y` lies in the range of `f` if and only if there exists an element `x` from `G` such that `f x` equals `y`. In other words, an element `y` of `N` is in the image of the additive monoid homomorphism `f` if and only if `y` is the image of some element in `G` under the function `f`. More concisely: An additive monoid homomorphism maps elements of its domain to elements in its range, and the range contains a given element if and only if there exists a preimage in the domain.
`Subgroup.mem_bot` theorem Subgroup.mem_bot : ∀ {G : Type u_1} [inst : Group G] {x : G}, x ∈ ⊥ ↔ x = 1 This theorem, `Subgroup.mem_bot`, states that for any type `G` which has a group structure (denoted by `Group G`), an element `x` of type `G` belongs to the trivial subgroup (denoted by `⊥`) if and only if `x` is the identity element of the group (denoted by `1`). The trivial subgroup is the subgroup consisting only of the identity element. Hence, in simple terms, in any group, an element is in the trivial subgroup if and only if it is the identity element. More concisely: In any group, an element is in the trivial subgroup if and only if it is the identity element.
`AddSubgroup.coeSubtype` theorem AddSubgroup.coeSubtype : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), ⇑H.subtype = Subtype.val The theorem `AddSubgroup.coeSubtype` asserts that for any additive group `G` and any subgroup `H` of `G`, the group homomorphism from the subgroup `H` to the group `G` (given by the `AddSubgroup.subtype` function) is equivalent to the underlying element in the base type (given by the `Subtype.val` function). In other words, applying the homomorphism to an element of the subgroup yields the same result as just taking the underlying element of the group. More concisely: For any additive group G and its subgroup H, the group homomorphism from H to G given by AddSubgroup.subtype is the same as the identity function on underling elements.
`AddSubgroup.coe_map` theorem AddSubgroup.coe_map : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (K : AddSubgroup G), ↑(AddSubgroup.map f K) = ⇑f '' ↑K The theorem `AddSubgroup.coe_map` asserts that for any given `AddGroup` G and `AddGroup` N, along with an additive homomorphism `f` from G to N and an `AddSubgroup` K of G, the image of the subgroup K under the map f is exactly the same as the image of the elements of K under the map f. In other words, the mapping of the subgroup K under the homomorphism f is equivalent to the set of elements obtained by mapping each element of K under f, represented in set-theoretic notation as `f(K)`. More concisely: For any additive homomorphism from an additive group to another group and any additive subgroup of the domain, the image of the subgroup under the homomorphism is equal to the set of images of its elements under the homomorphism.
`Subgroup.div_mem` theorem Subgroup.div_mem : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) {x y : G}, x ∈ H → y ∈ H → x / y ∈ H := by sorry This theorem states that a subgroup is closed under division. Specifically, for any type `G` that has a group structure, and any subgroup `H` of `G`, if `x` and `y` are elements of `H`, then the result of dividing `x` by `y` is also an element of `H`. Here, division is defined as per the group structure on `G`. More concisely: If `G` is a group type and `H` is a subgroup of `G`, then for all `x, y ∈ H`, `x / y ∈ H` where `/` is the division operation defined by the group structure on `G`.
`Subgroup.comap_normalizer_eq_of_surjective` theorem Subgroup.comap_normalizer_eq_of_surjective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H : Subgroup G) {f : N →* G}, Function.Surjective ⇑f → Subgroup.comap f H.normalizer = (Subgroup.comap f H).normalizer The theorem `Subgroup.comap_normalizer_eq_of_surjective` states that for any surjective monoid homomorphism `f` from a group `N` to another group `G`, and for any subgroup `H` of `G`, the preimage of the normalizer of `H` under `f` is equal to the normalizer of the preimage of `H` under `f`. In mathematical terms, if `f` is surjective, then the normalizer in `N` of the preimage of `H` equals the preimage in `N` of the normalizer of `H` in `G`. This links the concepts of preimages, normalizers, and surjective functions in the context of groups and subgroups. More concisely: For any surjective group homomorphism `f` and subgroup `H` of a group `G`, the normalizer of `f''(H)` in `N = domain(f)` equals the preimage of the normalizer of `H` in `G`.
`Subgroup.one_mem` theorem Subgroup.one_mem : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), 1 ∈ H This theorem states that for any given subgroup `H` of a group `G`, the identity element (or the "1") of the group `G` is always an element of the subgroup `H`. This is a fundamental property of subgroups in group theory. In other words, no matter what specific subgroup you have, it always includes the identity element of the overall group. More concisely: For any subgroup H of a group G, the identity element of G belongs to H.
`Mathlib.GroupTheory.Subgroup.Basic._auxAddLemma.76` theorem Mathlib.GroupTheory.Subgroup.Basic._auxAddLemma.76 : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} {h : ↥K}, (h ∈ H.addSubgroupOf K) = (↑h ∈ H) This theorem states that for any type `G` equipped with an additive group structure, and any subgroups `H` and `K` of `G`, an element `h` of `K` is in the intersection of `H` and `K` (as viewed as a subgroup of `K`) if and only if the underlying element of `h` in `G` is in `H`. In other words, it connects the membership of an element in the intersected subgroup with its membership in the original subgroup `H`. More concisely: For any additive group `G`, subgroups `H` and `K` of `G`, and `h` in `G`, `h` is in the intersection of `H` and `K` if and only if `h` is in `H`.
`AddSubgroup.mem_closure_singleton` theorem AddSubgroup.mem_closure_singleton : ∀ {G : Type u_1} [inst : AddGroup G] {x y : G}, y ∈ AddSubgroup.closure {x} ↔ ∃ n, n • x = y This theorem states that for any `AddGroup` `G` and any elements `x` and `y` of `G`, `y` is in the additive subgroup generated by `{x}` if and only if there exists a natural number `n` such that `n` times `x` equals `y`. In other words, the additive subgroup generated by a single element `x` of an additive group `G` is precisely the set of all integer multiples of `x`, i.e., it consists of all elements formed by adding `x` to itself `n` times for some integer `n`. More concisely: For any `AddGroup` `G` and element `x` in `G`, the additive subgroup generated by `{x}` equals the set of all elements `y` in `G` such that `y` can be expressed as `n x` for some natural number `n`.*
`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.69` theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.69 : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {K : Subgroup N} {f : G →* N} {x : G}, (x ∈ Subgroup.comap f K) = (f x ∈ K) This theorem states that for any groups `G` and `N`, a subgroup `K` of `N`, a group homomorphism `f` from `G` to `N`, and any element `x` of `G`, `x` is an element of the preimage subgroup of `K` under `f` if and only if the image of `x` under `f` is an element of `K`. In mathematical terms, this is saying that for any $x \in G$, $x \in f^{-1}(K)$ if and only if $f(x) \in K$. More concisely: For any group homomorphism $f$ from group $G$ to group $N$ and subgroup $K$ of $N$, $x \in G$ lies in the preimage $f^{-1}(K)$ if and only if $f(x) \in K$.
`Subgroup.ker_le_comap` theorem Subgroup.ker_le_comap : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) (H : Subgroup N), f.ker ≤ Subgroup.comap f H This theorem states that for any given group homomorphism `f` from a group `G` to another group `N`, and any subgroup `H` of `N`, the multiplicative kernel of `f` is a subset of (or equal to) the preimage of `H` under `f`. The multiplicative kernel of `f` here refers to the set of all elements `x` in `G` such that `f(x)` equals the identity element in `N`. The preimage of `H` under `f` is the set of all elements in `G` that map to any element in `H` under `f`. More concisely: The multiplicative kernel of a group homomorphism is contained in the preimage of its subgroup under the homomorphism.
`AddSubgroup.mem_top` theorem AddSubgroup.mem_top : ∀ {G : Type u_1} [inst : AddGroup G] (x : G), x ∈ ⊤ This theorem states that for all types `G`, given that `G` has an `AddGroup` instance, any element `x` of `G` belongs to the top additive subgroup. In other words, every element of an additive group is a member of the group's top (universal) subgroup. More concisely: For any additive group G, every element x of G belongs to its top additive subgroup.
`Subgroup.ext` theorem Subgroup.ext : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, (∀ (x : G), x ∈ H ↔ x ∈ K) → H = K := by sorry This theorem states that for any given group `G`, if there are two subgroups `H` and `K` of `G` such that a member `x` of group `G` belongs to `H` if and only if `x` also belongs to `K`, then the subgroups `H` and `K` are equal. In other words, two subgroups of a group are equal if and only if they contain exactly the same elements. More concisely: If two subgroups of a group have the same elements, then they are equal.
`AddSubgroup.zero_mem` theorem AddSubgroup.zero_mem : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), 0 ∈ H This theorem states that for any additive group `G` and any subgroup `H` of `G`, the zero element of the group is always an element of the subgroup. The zero element in the context of an additive group is the group's identity element. This is a fundamental property of subgroups in the context of group theory. More concisely: For any additive group G and subgroup H, the zero element of G is in H.
`AddSubgroup.map_le_iff_le_comap` theorem AddSubgroup.map_le_iff_le_comap : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {K : AddSubgroup G} {H : AddSubgroup N}, AddSubgroup.map f K ≤ H ↔ K ≤ AddSubgroup.comap f H The theorem `AddSubgroup.map_le_iff_le_comap` states that for any two additive groups `G` and `N`, and a homomorphism `f` from `G` to `N`, an additive subgroup `K` of `G`, and an additive subgroup `H` of `N`, the image of `K` under `f` is a subgroup of `H` if and only if `K` is a subgroup of the preimage of `H` under `f`. In other words, it provides a criterion for comparing an original subgroup and its image or how a subgroup in the target relates to a subgroup in the source via the homomorphism. More concisely: For additive groups G, N, homomorphism f: G -> N, subgroups K of G, and H of N, the image of K under f is a subgroup of H if and only if K is a subgroup of the preimage of H under f.
`AddMonoidHom.map_range` theorem AddMonoidHom.map_range : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} {P : Type u_6} [inst_1 : AddGroup N] [inst_2 : AddGroup P] (g : N →+ P) (f : G →+ N), AddSubgroup.map g f.range = (g.comp f).range The theorem `AddMonoidHom.map_range` states that for any two additive group homomorphisms `f` and `g`, where `f` is from an additive group `G` to an additive group `N` and `g` is from `N` to another additive group `P`, the range of the composition of `f` and `g` (denoted as `AddMonoidHom.range (AddMonoidHom.comp g f)`) is equal to the image of the range of `f` under the map `g` (denoted as `AddSubgroup.map g (AddMonoidHom.range f)`). In other words, this theorem guarantees the commutativity of taking the range of a homomorphism and taking the image of a subgroup in the context of additive group theory. More concisely: The range of the composition of two additive group homomorphisms is equal to the image of the range of the first homomorphism under the second homomorphism.
`Subgroup.inclusion_injective` theorem Subgroup.inclusion_injective : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} (h : H ≤ K), Function.Injective ⇑(Subgroup.inclusion h) := by sorry This theorem asserts that for any given type `G` with a `Group` instance and any two subgroups `H` and `K` of `G`, if `H` is a subset of `K`, then the inclusion homomorphism from `H` to `K` is injective. In other words, if we have two elements from `H` and they map to the same element in `K` through the inclusion homomorphism, then these two elements were originally the same element in `H`. More concisely: If `H` is a subgroup of `K` in a group `G`, then the inclusion homomorphism from `H` to `K` is an injection.
`Subgroup.nontrivial_iff_exists_ne_one` theorem Subgroup.nontrivial_iff_exists_ne_one : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), Nontrivial ↥H ↔ ∃ x ∈ H, x ≠ 1 This theorem states that for any type `G` with a group structure and for any subgroup `H` of `G`, `H` is nontrivial (i.e., `H` contains at least two distinct elements) if and only if there exists an element `x` in `H` such that `x` is not the identity element of the group. In other words, a subgroup is nontrivial if it contains an element other than the group's identity. More concisely: A subgroup of a group is nontrivial if and only if it contains a non-identity element.
`AddSubgroup.normal_addSubgroupOf_iff` theorem AddSubgroup.normal_addSubgroupOf_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H ≤ K → ((H.addSubgroupOf K).Normal ↔ ∀ (h k : G), h ∈ H → k ∈ K → k + h + -k ∈ H) The theorem `AddSubgroup.normal_addSubgroupOf_iff` states that for any type `G` with an addition group structure and any subgroups `H` and `K` of `G`, if `H` is a subset of `K`, then the subgroup `H` is normal within `K` (viewed as a subgroup of `K`), if and only if for any elements `h` in `H` and `k` in `K`, the element resulting from the operation `k + h + -k` is also in `H`. Here, '+' denotes the addition operation in the group, and '-' denotes the additive inverse. This theorem thus establishes a criterion for normality of a subgroup within another subgroup in the context of additive groups. More concisely: A subgroup H of an additive group G is normal in another subgroup K if and only if for all h in H and k in K, k + h - k is in H.
`InvMemClass.inv_mem` theorem InvMemClass.inv_mem : ∀ {S : Type u_5} {G : Type u_6} [inst : Inv G] [inst_1 : SetLike S G] [self : InvMemClass S G] {s : S} {x : G}, x ∈ s → x⁻¹ ∈ s This theorem states that if a set `s` of elements of type `G` is closed under inverses, then for any element `x` of type `G` that belongs to set `s`, the inverse of `x` (denoted as `x⁻¹`) also belongs to the set `s`. The elements of type `G` are assumed to have an inverse operation defined on them as indicated by the `Inv G` instance. The `SetLike S G` instance states that `S` behaves like a set of `G`. The `InvMemClass S G` instance states that `S` is a class of `G` that is closed under inverses. More concisely: If `s` is a set of elements of type `G` that is closed under inverses, then for every `x` in `s`, the inverse `x⁻¹` is also in `s`.
`Subgroup.map_comap_eq_self` theorem Subgroup.map_comap_eq_self : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {H : Subgroup N}, H ≤ f.range → Subgroup.map f (Subgroup.comap f H) = H The theorem `Subgroup.map_comap_eq_self` states that for any group homomorphism `f` from a group `G` to a group `N` and a subgroup `H` of `N`, if `H` is a subset of the range of `f`, then the image of the preimage of `H` under `f` is `H` itself. In other words, if we first use `f` to pull back `H` to a subgroup of `G`, and then push that forward under `f`, we recover `H`. This is a common pattern in the theory of groups, reflecting the idea that the image of the preimage of a set under a function should coincide with the original set, whenever the set is included in the range of the function. More concisely: For any group homomorphism `f` and subgroup `H` of a group `N` with `H` contained in the image of `f`, the preimage `f⁻¹[H]` under `f` equals `H`.
`Subgroup.map_equiv_normalizer_eq` theorem Subgroup.map_equiv_normalizer_eq : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H : Subgroup G) (f : G ≃* N), Subgroup.map f.toMonoidHom H.normalizer = (Subgroup.map f.toMonoidHom H).normalizer The theorem `Subgroup.map_equiv_normalizer_eq` states that for any two groups `G` and `N`, and any subgroup `H` of `G`, if there exists an isomorphism `f` from `G` to `N`, then the image of the normalizer of `H` under `f` is equal to the normalizer of the image of `H` under `f`. In simpler terms, it says that the operation of taking the normalizer commutes with the operation of taking the image under a group isomorphism. This theorem relates the concept of normalizer of a subgroup in one group with the corresponding concept in another group under a group isomorphism. More concisely: For any groups G, N, and subgroup H of G, if there exists an isomorphism f from G to N, then Norm(H)^f = Norm(f(H)) where Norm(X) denotes the normalizer of subgroup X.
`Subgroup.normal_le_normalCore` theorem Subgroup.normal_le_normalCore : ∀ {G : Type u_1} [inst : Group G] {H N : Subgroup G} [hN : N.Normal], N ≤ H.normalCore ↔ N ≤ H This theorem states that for any group `G`, and any subgroups `H` and `N` of `G`, where `N` is a normal subgroup, `N` is a subset of the normal core of `H` if and only if `N` is a subset of `H`. The normal core of a subgroup `H` is the largest normal subgroup of `G` that is contained in `H`. Therefore, this theorem essentially says that a normal subgroup `N` can only be part of the normal core of `H` if it is also part of `H` itself. More concisely: For any group `G`, a normal subgroup `N` of `G` is contained in the normal core of a subgroup `H` of `G` if and only if `N` is a subset of `H`.
`AddMonoidHom.ker_eq_bot_iff` theorem AddMonoidHom.ker_eq_bot_iff : ∀ {G : Type u_1} [inst : AddGroup G] {M : Type u_7} [inst_1 : AddZeroClass M] (f : G →+ M), f.ker = ⊥ ↔ Function.Injective ⇑f This theorem states that for any additive group `G` and any type `M` with an additive zero, for any additive monoid homomorphism `f` from `G` to `M`, the kernel of `f` is the trivial group if and only if `f` is injective. In other words, `f` has no non-zero elements in `G` mapping to the zero of `M` if and only if no two distinct elements in `G` map to the same element in `M` under `f`. More concisely: For any additive group homomorphism from an additive group to a group with an additive zero, the kernel is the trivial group if and only if the homomorphism is injective.
`Subgroup.Normal.conj_mem` theorem Subgroup.Normal.conj_mem : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.Normal → ∀ n ∈ H, ∀ (g : G), g * n * g⁻¹ ∈ H This theorem states that for any group `G`, if `H` is a normal subgroup of `G`, then `H` is closed under conjugation. Specifically, for any element `n` in `H` and any group element `g`, the conjugate of `n` by `g` (which is calculated as `g * n * g⁻¹`) still belongs to `H`. This is a property intrinsic to normal subgroups in group theory. More concisely: In a group, if a subgroup is normal, then its elements are closed under conjugation.
`Subgroup.comap_map_eq` theorem Subgroup.comap_map_eq : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) (H : Subgroup G), Subgroup.comap f (Subgroup.map f H) = H ⊔ f.ker The theorem `Subgroup.comap_map_eq` states that for any group homomorphism `f` from a group `G` to a group `N`, and for any subgroup `H` of `G`, the subgroup obtained by first mapping `H` under `f` and then taking the preimage under `f` is equal to the join of `H` and the kernel of `f`. In other words, when you map a subgroup to another group and then pull it back, you not only get the original subgroup, but also the elements of the original group that are mapped to the identity in the target group. More concisely: For any group homomorphism `f` and subgroup `H` of a group `G`, `f''(H) = H.join (f.ker)`, where `f''` denotes the image of `H` under `f` and `join` denotes the subgroup generated by the union of two subgroups.
`AddMonoidHom.range_top_of_surjective` theorem AddMonoidHom.range_top_of_surjective : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_7} [inst_1 : AddGroup N] (f : G →+ N), Function.Surjective ⇑f → f.range = ⊤ The theorem `AddMonoidHom.range_top_of_surjective` states that for any `AddGroup` types G and N, if a function `f` is an `AddMonoid` homomorphism from G to N and is surjective (i.e., for every element in the codomain N, there exists an element in the domain G such that the function applied to that element yields the given element in N), then the range of this function is the entire codomain N. In other words, the surjective `AddMonoid` homomorphism fully covers the codomain. More concisely: If `f` is a surjective `AddMonoid` homomorphism from an `AddGroup` `G` to another `AddGroup` `N`, then the range of `f` is all of `N`.
`Subgroup.inv_mem'` theorem Subgroup.inv_mem' : ∀ {G : Type u_5} [inst : Group G] (self : Subgroup G) {x : G}, x ∈ self.carrier → x⁻¹ ∈ self.carrier This theorem states that for any group `G`, if `x` is an element of the carrier of a subgroup of `G`, then the inverse of `x` (denoted as `x⁻¹`) is also an element of that subgroup's carrier. In other words, the set that forms the subgroup is closed under the operation of taking inverses, which is a necessary condition for a subset to be a subgroup in group theory. More concisely: If `G` is a group and `S` is a subgroup of `G`, then for all `x ∈ S`, we have `x⁻¹ ∈ S`.
`Subgroup.mem_comap` theorem Subgroup.mem_comap : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {K : Subgroup N} {f : G →* N} {x : G}, x ∈ Subgroup.comap f K ↔ f x ∈ K This theorem states that for any groups `G` and `N`, any subgroup `K` of `N`, any group homomorphism `f` from `G` to `N`, and any element `x` of `G`, the element `x` belongs to the preimage of subgroup `K` along the homomorphism `f` if and only if the image of `x` under `f` belongs to `K`. Here, the preimage of a subgroup along a homomorphism is defined as the subgroup of `G` consisting of all elements which map to `K` under `f`. More concisely: For any group homomorphism $f$ from group $G$ to group $N$, subgroup $K$ of $N$, and element $x$ in $G$, $x$ is in the preimage of $K$ under $f$ if and only if $f(x) \in K$.
`normalizerCondition_iff_only_full_group_self_normalizing` theorem normalizerCondition_iff_only_full_group_self_normalizing : ∀ {G : Type u_1} [inst : Group G], NormalizerCondition G ↔ ∀ (H : Subgroup G), H.normalizer = H → H = ⊤ This theorem provides an alternative formulation of the Normalizer Condition for a group `G`. It states that the Normalizer Condition holds for a group `G` if and only if for every subgroup `H` of `G`, the normalizer of subgroup `H` equals `H` implies that `H` is the full group `G`. This version might be more convenient to use because it avoids the need for inequalities and negations. This statement can be equivalently expressed saying that in a group satisfying the Normalizer Condition, only the full group is self-normalizing, or in other words, it is its own normalizer. More concisely: In a group satisfying the Normalizer Condition, only the full group is self-normalizing.
`add_mem_cancel_left` theorem add_mem_cancel_left : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_6} {H : S} [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G] {x y : G}, x ∈ H → (x + y ∈ H ↔ y ∈ H) This theorem states that for any given type `G` with an addition group structure, a type `S`, an instance `H` of `S`, and two elements `x` and `y` of `G`, if `x` is in `H` (where `H` is treated as a set of elements of type `G` by the `SetLike S G` instance), then `y` is in `H` if and only if the sum of `x` and `y` is in `H`. Note that `H` is assumed to be an additive subgroup of `G` due to the `AddSubgroupClass S G` instance. More concisely: For any additive subgroup `H` of a group `G`, if `x` is an element of `H` and `x + y` is an element of `G`, then `y` is an element of `H`.
`AddSubgroup.le_normalizer_comap` theorem AddSubgroup.le_normalizer_comap : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {N : Type u_5} [inst_1 : AddGroup N] (f : N →+ G), AddSubgroup.comap f H.normalizer ≤ (AddSubgroup.comap f H).normalizer The theorem `AddSubgroup.le_normalizer_comap` states that for any additive group `G`, any additive subgroup `H` of `G`, any other additive group `N`, and any additive group homomorphism `f` from `N` to `G`, the preimage of the normalizer of `H` under `f` is contained in the normalizer of the preimage of `H` under `f`. In other words, if you first find the normalizer of a subgroup and then take the preimage under a homomorphism, you will end up with a set that is within the set you get if you first take the preimage of the subgroup and then find its normalizer. More concisely: For any additive groups G, H, and any additive group homomorphism f from N to G, the normalizer of f(H) in G contains f(N\_H), where N\_H is the normalizer of H in N.
`Subgroup.le_normalizer_map` theorem Subgroup.le_normalizer_map : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {N : Type u_5} [inst_1 : Group N] (f : G →* N), Subgroup.map f H.normalizer ≤ (Subgroup.map f H).normalizer The theorem `Subgroup.le_normalizer_map` states that for any group `G` with a subgroup `H`, and any group `N`, if there is a monoid homomorphism `f` from `G` to `N`, then the image of the normalizer of `H` under this map is a subgroup of or equal to the normalizer of the image of `H` under the same map. In mathematical terms, this can be expressed as $f(N_G(H)) \subseteq N_{G'}(f(H))$, where $N_G(H)$ denotes the normalizer of `H` in `G` and $N_{G'}(f(H))$ denotes the normalizer of `f(H)` in `N`. More concisely: The normalizer of a subgroup in a group is mapped to the normalizer of its image under any monoid homomorphism.
`Subgroup.Normal.mem_comm_iff` theorem Subgroup.Normal.mem_comm_iff : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.Normal → ∀ {a b : G}, a * b ∈ H ↔ b * a ∈ H This theorem states that for any group `G` and any subgroup `H` of `G`, if `H` is a normal subgroup, then for any two elements `a` and `b` of `G`, `a * b` is in `H` if and only if `b * a` is in `H`. Here `` denotes the group operation in `G`. This means, in the context of group theory, that the product of `a` and `b` belongs to the subgroup `H` if and only if the product of `b` and `a` (i.e., the order of multiplication is reversed) also belongs to `H`. More concisely: If `H` is a normal subgroup of group `G`, then for all `a, b` in `G`, `a * b` is in `H` if and only if `b * a` is in `H`.*
`AddSubgroup.Normal.comap` theorem AddSubgroup.Normal.comap : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {H : AddSubgroup N}, H.Normal → ∀ (f : G →+ N), (AddSubgroup.comap f H).Normal The theorem `AddSubgroup.Normal.comap` states that for any two types `G` and `N` where both `G` and `N` are additive groups, and for any additive subgroup `H` of `N` that is normal, for any additive monoid homomorphism `f` from `G` to `N`, the preimage of `H` under `f`, which is an additive subgroup of `G`, is also normal. In other words, the preimage of a normal subgroup under an additive monoid homomorphism is still a normal subgroup. More concisely: If `G` and `N` are additive groups, `H` is a normal additive subgroup of `N`, and `f` is an additive monoid homomorphism from `G` to `N`, then the preimage of `H` under `f` is a normal additive subgroup of `G`.
`AddSubgroup.closure_induction'` theorem AddSubgroup.closure_induction' : ∀ {G : Type u_1} [inst : AddGroup G] {k : Set G} {p : (x : G) → x ∈ AddSubgroup.closure k → Prop}, (∀ (x : G) (h : x ∈ k), p x ⋯) → p 0 ⋯ → (∀ (x : G) (hx : x ∈ AddSubgroup.closure k) (y : G) (hy : y ∈ AddSubgroup.closure k), p x hx → p y hy → p (x + y) ⋯) → (∀ (x : G) (hx : x ∈ AddSubgroup.closure k), p x hx → p (-x) ⋯) → ∀ {x : G} (hx : x ∈ AddSubgroup.closure k), p x hx The theorem `AddSubgroup.closure_induction'` states that for any type `G` with an `AddGroup` instance and for any set `k` of `G`, given a property `p` that depends on an element of `G` and a proof that said element belongs to the additive subgroup generated by `k`, if `p` holds for every element of `k`, and `p` holds for the additive identity `0`, and `p` holds for the sum of any two elements of the additive subgroup generated by `k` provided `p` holds separately for each of these two elements, and `p` holds for the additive inverse of any element of the additive subgroup generated by `k` provided `p` holds for that element, then `p` holds for every element of the additive subgroup generated by `k`. In simpler terms, it provides a principle of mathematical induction for additive subgroups generated by sets. More concisely: If `G` is an add group, `k` is a set of `G`, and `p` holds for every element in `k`, `0`, the sum of any two elements in the additive subgroup generated by `k`, and the additive inverse of any element in the subgroup, then `p` holds for every element in the additive subgroup generated by `k`.
`AddSubgroup.coe_neg` theorem AddSubgroup.coe_neg : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (x : ↥H), ↑(-x) = -↑x This theorem states that for any specific AddGroup `G` and any element `x` in an AddSubgroup `H` of `G`, the negation of `x` in the group (expressed as `-x`) when coerced (or converted) back to its underlying type is equal to the negative of the coercion of `x` (expressed as `-↑x`). Essentially, this theorem asserts that the negation operation in the subgroup is consistent with the negation operation in the larger group. More concisely: For any AddGroup `G`, AddSubgroup `H` within `G`, and element `x` in `H`, the negation of `x` in `H` (`-x`) is equal to the negative of `x` in `G` coerced back to `H` (`-↑x`).
`Subgroup.bot_or_exists_ne_one` theorem Subgroup.bot_or_exists_ne_one : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H = ⊥ ∨ ∃ x ∈ H, x ≠ 1 := by sorry This theorem states that, for any group `G` and any subgroup `H` of `G`, `H` is either the trivial subgroup (denoted by `⊥`) or there exists an element `x` in `H` which is not the identity element (`1`). In other words, every subgroup of a group is either the group containing only the identity element or has at least one element different from the identity. More concisely: Every subgroup of a group is either the trivial subgroup or contains an element not equal to the identity.
`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.71` theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.71 : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {K : Subgroup G} {y : N}, (y ∈ Subgroup.map f K) = ∃ x ∈ K, f x = y This theorem states that for any groups `G` and `N`, a group homomorphism `f` from `G` to `N`, a subgroup `K` of `G`, and an element `y` of `N`, `y` is in the image of the subgroup `K` under the homomorphism `f` if and only if there exists an element `x` in `K` such that `f(x)` equals `y`. In other words, it characterizes the image of a subgroup under a group homomorphism in terms of the elements of the original subgroup and the homomorphism's action on them. More concisely: For any group homomorphism $f$ from group $G$ to group $N$, subgroup $K$ of $G$, and element $y$ in $N$, $y$ is in the image of $K$ under $f$ if and only if there exists an element $x$ in $K$ such that $f(x) = y$.
`Subgroup.map_equiv_eq_comap_symm'` theorem Subgroup.map_equiv_eq_comap_symm' : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G ≃* N) (K : Subgroup G), Subgroup.map f.toMonoidHom K = Subgroup.comap f.symm.toMonoidHom K This theorem states that for any groups `G` and `N`, and a multiplicative equivalence `f` from `G` to `N`, the image of a subgroup `K` of `G` under the monoid homomorphism induced by `f` is the same as the preimage of `K` under the monoid homomorphism induced by the inverse of `f`. In other words, mapping `K` through `f` and then pulling it back via the inverse of `f` gives us `K` back. This is a manifestation of the fundamental property of isomorphisms (or equivalences) in group theory. More concisely: For any group homomorphism `f` and subgroup `K` of groups `G` and `N`, `f(K) = (f^(-1))^(-1)(K)`.
`AddMonoidHom.range_top_iff_surjective` theorem AddMonoidHom.range_top_iff_surjective : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_7} [inst_1 : AddGroup N] {f : G →+ N}, f.range = ⊤ ↔ Function.Surjective ⇑f This theorem states that for any given additive group `G`, another additive group `N`, and an additive monoid homomorphism `f` from `G` to `N`, the range of `f` is the entire group `N` (denoted as `⊤`) if and only if `f` is a surjective function. In other words, `f` maps every element of `G` onto every element of `N` if and only if every element of `N` is the image of some element of `G` under the function `f`. More concisely: For an additive group homomorphism from an additive group to an additive group, the image of the homomorphism is the entire group if and only if the homomorphism is surjective.
`Subgroup.normal_subgroupOf_iff` theorem Subgroup.normal_subgroupOf_iff : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H ≤ K → ((H.subgroupOf K).Normal ↔ ∀ (h k : G), h ∈ H → k ∈ K → k * h * k⁻¹ ∈ H) The theorem `Subgroup.normal_subgroupOf_iff` states that, for any group `G` and any subgroups `H` and `K` of `G`, if `H` is a subgroup of `K`, then `H` is a normal subgroup of `K` (i.e., `Subgroup.subgroupOf H K` is a normal subgroup) if and only if for all elements `h` in `H` and `k` in `K`, the element `k * h * k⁻¹` (the conjugate of `h` by `k`) is also in `H`. In the language of group theory, this is saying that a subgroup is normal if and only if it is closed under conjugation by elements of the larger group. More concisely: A subgroup of a group is normal if and only if it is closed under conjugation by elements of the group.
`Subgroup.map_comap_eq` theorem Subgroup.map_comap_eq : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) (H : Subgroup N), Subgroup.map f (Subgroup.comap f H) = f.range ⊓ H The theorem `Subgroup.map_comap_eq` states that for any group homomorphism `f` from a group `G` to another group `N` and any subgroup `H` of `N`, the image under `f` of the preimage under `f` of `H` is equal to the intersection of the range of `f` and `H`. In other words, if we first take the preimage of `H` under `f` in `G` and then map it back to `N` using `f`, we get exactly the elements in the range of `f` that are also in `H`. More concisely: The image of the preimage of a subgroup under a group homomorphism is equal to the intersection of the range of the homomorphism and the subgroup.
`Subgroup.eq_top_iff'` theorem Subgroup.eq_top_iff' : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H = ⊤ ↔ ∀ (x : G), x ∈ H This theorem states that for any subgroup `H` of a group `G`, `H` is equal to the top element (i.e., the whole group `G`) if and only if every element `x` in `G` is also in `H`. In other words, a subgroup is identical to the whole group if all elements of the group are contained in the subgroup. More concisely: A subgroup of a group is equal to the whole group if and only if it contains every element of the group.
`Subgroup.subset_closure` theorem Subgroup.subset_closure : ∀ {G : Type u_1} [inst : Group G] {k : Set G}, k ⊆ ↑(Subgroup.closure k) This theorem states that for any set `k` of elements in a group `G`, the set `k` is a subset of the subgroup generated by `k`. In other words, every element in `k` is also an element in the subgroup produced by the `Subgroup.closure` function applied to `k`. This ensures that the closure operation indeed encapsulates all members of the original set `k` within the produced subgroup in the group `G`. More concisely: For any set `k` of elements in a group `G`, `k` is a subset of the subgroup generated by `k` (i.e., the subgroup generated by `k` contains every element in `k`).
`Mathlib.GroupTheory.Subgroup.Basic._auxAddLemma.89` theorem Mathlib.GroupTheory.Subgroup.Basic._auxAddLemma.89 : ∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → AddGroup (f i)] (I : Set η) {H : (i : η) → AddSubgroup (f i)} {p : (i : η) → f i}, (p ∈ AddSubgroup.pi I H) = ∀ i ∈ I, p i ∈ H i This theorem states that for any type `η`, any function `f` from `η` to another type, any set `I` of type `η`, and any function `H` that assigns to each element of `η` an additive subgroup of `f i`, a function `p` from `η` to `f i` is in the additive subgroup `pi I H` (which is the set of functions whose values are in the corresponding additive subgroup for each index in `I`) if and only if for every element `i` in `I`, the value `p i` is in the additive subgroup `H i`. More concisely: For any type `η`, function `f` from `η` to another type, set `I` of type `η`, and function `H` that assigns to each element of `η` an additive subgroup of `f i`, a function `p` from `η` to `fi` is in the additive subgroup `pi I H` if and only if `p i` is in `Hi` for all `i` in `I`.
`Subgroup.characteristic_iff_comap_le` theorem Subgroup.characteristic_iff_comap_le : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.Characteristic ↔ ∀ (ϕ : G ≃* G), Subgroup.comap ϕ.toMonoidHom H ≤ H This theorem states that for any group 'G' and subgroup 'H' of 'G', the subgroup 'H' is characteristic if and only if for every bijective multiplication-preserving function 'ϕ' from 'G' to 'G' (also known as a group automorphism), the preimage of 'H' under the group homomorphism induced by 'ϕ' is a subset of 'H'. In other words, a subgroup is characteristic if it is invariant under any automorphism of the group. More concisely: A subgroup of a group is characteristic if and only if it is mapped to itself under every group automorphism.
`MonoidHom.ker_eq_bot_iff` theorem MonoidHom.ker_eq_bot_iff : ∀ {G : Type u_1} [inst : Group G] {M : Type u_7} [inst_1 : MulOneClass M] (f : G →* M), f.ker = ⊥ ↔ Function.Injective ⇑f The theorem `MonoidHom.ker_eq_bot_iff` states that for any group `G` and any type `M` endowed with multiplication and an identity element, a monoid homomorphism `f: G → M` has a trivial kernel (the kernel of `f` is the trivial subgroup, denoted by `⊥`) if and only if `f` is injective. In other words, in the context of group theory, a monoid homomorphism between a group and a mul-one-class is injective exactly when the preimage of the identity element under the homomorphism is just the identity element of the group. More concisely: A monoid homomorphism from a group to a monoid with an identity is injective if and only if its kernel is the trivial subgroup.
`MonoidHom.range_top_of_surjective` theorem MonoidHom.range_top_of_surjective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_7} [inst_1 : Group N] (f : G →* N), Function.Surjective ⇑f → f.range = ⊤ The theorem `MonoidHom.range_top_of_surjective` states that for any given groups `G` and `N`, if a monoid homomorphism `f` exists from `G` to `N` that is surjective (i.e., every element of `N` is the image of some element in `G` under `f`), then the range of `f` equals the entire group `N`. In other words, a surjective monoid homomorphism maps its domain onto the entirety of its codomain. More concisely: If `f` is a surjective monoid homomorphism from group `G` to group `N`, then the range of `f` equals `N`.
`AddSubgroup.map_map` theorem AddSubgroup.map_map : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) {N : Type u_5} [inst_1 : AddGroup N] {P : Type u_6} [inst_2 : AddGroup P] (g : N →+ P) (f : G →+ N), AddSubgroup.map g (AddSubgroup.map f K) = AddSubgroup.map (g.comp f) K The theorem `AddSubgroup.map_map` states that for any additive groups `G`, `N`, and `P`, any subgroup `K` of `G`, and any additive monoid homomorphisms `f` from `G` to `N` and `g` from `N` to `P`, the image of the subgroup `K` under the composite homomorphism `g ∘ f` is the same as the image of the image of `K` under `f` under `g`. In other words, the `map` operation on subgroups is compatible with the composition of homomorphisms, or in notation, `AddSubgroup.map g (AddSubgroup.map f K) = AddSubgroup.map (AddMonoidHom.comp g f) K`. This is an instance of a basic property in abstract algebra stating that homomorphisms respect the structure of groups. More concisely: For any additive groups G, N, and P, subgroup K of G, and additive monoid homomorphisms f : G -> N and g : N -> P, the image of K under the composite homomorphism g ∘ f is equal to the image of the image of K under f, then under g. (AddSubgroup.map g (AddSubgroup.map f K) = AddSubgroup.map (AddMonoidHom.comp g f) K)
`Subgroup.map_normalClosure` theorem Subgroup.map_normalClosure : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (s : Set G) (f : G →* N), Function.Surjective ⇑f → Subgroup.map f (Subgroup.normalClosure s) = Subgroup.normalClosure (⇑f '' s) This theorem states that for any set `s` of elements of a group `G` and any surjective monoid homomorphism `f` from `G` to another group `N`, the image of the normal closure of `s` under the homomorphism `f` is equal to the normal closure of the image of `s` under `f`. In other words, the process of taking normal closures commutes with the process of taking images under a surjective homomorphism. This implies that the structure of the normal closure of a set in a group is preserved under surjective homomorphisms. More concisely: For any surjective group homomorphism `f` and set `s` in a group `G`, the normal closure of `f(s)` in `N = f(NormalClosure(s, G))`.
`Subgroup.map_equiv_eq_comap_symm` theorem Subgroup.map_equiv_eq_comap_symm : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G ≃* N) (K : Subgroup G), Subgroup.map (↑f) K = Subgroup.comap (↑f.symm) K This theorem states that for any given groups `G` and `N`, an isomorphism `f` from `G` to `N`, and a subgroup `K` of `G`, the image of `K` under `f` (denoted by `Subgroup.map (↑f) K`) is the same as the preimage of `K` under the inverse of `f` (denoted by `Subgroup.comap (↑(MulEquiv.symm f)) K`). In other words, mapping a subgroup through an isomorphism and taking the preimage of the same subgroup through the inverse of that isomorphism result in the same subgroup. More concisely: For any groups G, N, an isomorphism f between them, and a subgroup K of G, the image of K under f and the preimage of K under the inverse of f are equal. (Subgroup.map (↑f) K = Subgroup.comap (↑(MulEquiv.symm f)) K)
`Subgroup.closure_mono` theorem Subgroup.closure_mono : ∀ {G : Type u_1} [inst : Group G] ⦃h k : Set G⦄, h ⊆ k → Subgroup.closure h ≤ Subgroup.closure k The theorem `Subgroup.closure_mono` states that in any given group `G`, the subgroup closure operation is monotone with respect to set inclusion. In other words, if you have two sets of elements `h` and `k` from the group `G`, and `h` is a subset of `k` (denoted by `h ⊆ k`), then the subgroup generated by `h` is a subgroup of (or equal to) the subgroup generated by `k` (denoted by `Subgroup.closure h ≤ Subgroup.closure k`). This means that adding more elements to the generating set of a subgroup can only result in a larger subgroup. More concisely: In any group, the subgroup closure operation is monotone with respect to set inclusion, i.e., the subgroup generated by a subset is a subgroup of the subgroup generated by a larger subset.
`Subgroup.coe_top` theorem Subgroup.coe_top : ∀ {G : Type u_1} [inst : Group G], ↑⊤ = Set.univ This theorem, `Subgroup.coe_top`, states that for any group `G` of a certain type `u_1`, the top subgroup (denoted by `⊤`) of this group, when coerced (`↑`), is equal to the universal set (`Set.univ`). In other words, it asserts that the set of all elements in the top subgroup of a given group `G` is equivalent to the complete set containing all elements of the type of `G`. More concisely: The coercion of the top subgroup of a group to a set is equal to the universal set.
`AddSubgroup.neg_mem` theorem AddSubgroup.neg_mem : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) {x : G}, x ∈ H → -x ∈ H := by sorry This theorem states that for any type `G` that has an `AddGroup` instance and any `AddSubgroup` `H` of `G`, if an element `x` belongs to `H`, then its additive inverse `-x` also belongs to `H`. In other words, an additive subgroup is closed under taking inverses. More concisely: If `H` is an additive subgroup of the additive group `G`, then for all `x` in `H`, `-x` is also in `H`.
`AddSubgroup.closure_induction` theorem AddSubgroup.closure_induction : ∀ {G : Type u_1} [inst : AddGroup G] {k : Set G} {p : G → Prop} {x : G}, x ∈ AddSubgroup.closure k → (∀ x ∈ k, p x) → p 0 → (∀ (x y : G), p x → p y → p (x + y)) → (∀ (x : G), p x → p (-x)) → p x The theorem `AddSubgroup.closure_induction` states the following induction principle for membership in an additive closure: Given a type `G` with an additive group structure, a set `k` of type `G`, and a property `p` from `G` to `Prop`, for any element `x` of `G`, if `x` belongs to the additive closure of `k`, and if property `p` holds for all elements of `k`, for `0`, is preserved under addition (i.e., if `p` holds for `x` and `y`, then it also holds for `x + y`), and is preserved under taking additive inverses (i.e., if `p` holds for `x`, then it also holds for `-x`), then `p` holds for `x`. This principle can be used to prove properties of all elements of an additive closure, given that these properties hold for the generating set and are preserved under the group operations. More concisely: Given an additive group `(G, +)` and a subset `k` of `G`, if `x` is in the additive closure of `k`, and `p(y)` holds for all `y` in `k` and is closed under addition and additive inverses, then `p(x)` holds.
`AddSubgroup.bot_or_nontrivial` theorem AddSubgroup.bot_or_nontrivial : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H = ⊥ ∨ Nontrivial ↥H This theorem states that for any additive subgroup `H` of an additive group `G`, `H` is either equal to the trivial subgroup (denoted by `⊥`) or `H` is nontrivial. Here, a group is called trivial if it contains only one element, and nontrivial otherwise. In other words, any subgroup of a group is either a group with just one element, or it has more than one distinct element. More concisely: Every additive subgroup of an additive group is either the trivial subgroup or nontrivial.
`AddSubgroup.add_mem_cancel_right` theorem AddSubgroup.add_mem_cancel_right : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) {x y : G}, x ∈ H → (y + x ∈ H ↔ y ∈ H) This theorem is a property of addition in subgroups of an additive group. It states that for any type `G` that has an additive group structure, for any additive subgroup `H` of `G`, and for any elements `x` and `y` of `G`, if `x` is an element of `H`, then `y + x` is an element of `H` if and only if `y` is an element of `H`. In mathematical terms, given `x ∈ H`, the membership of `y + x` in `H` is equivalent to the membership of `y` in `H`. More concisely: For any additive subgroup `H` of an additive group `G` and any `x, y` in `G`, if `x` is in `H` then `y + x` is in `H` if and only if `y` is in `H`.
`MonoidHom.mem_ker` theorem MonoidHom.mem_ker : ∀ {G : Type u_1} [inst : Group G] {M : Type u_7} [inst_1 : MulOneClass M] (f : G →* M) {x : G}, x ∈ f.ker ↔ f x = 1 The theorem `MonoidHom.mem_ker` states that for any group `G`, any type `M` with a multiplication and a multiplicative identity, and any monoid homomorphism `f` from `G` to `M`, an element `x` of `G` belongs to the multiplicative kernel of `f` if and only if the evaluation of `f` at `x` equals the multiplicative identity of `M`. In mathematical terms, this is saying if `f : G → M` is a monoid homomorphism, then `x ∈ ker(f)` if and only if `f(x) = 1`, where `ker(f)` is the kernel of `f`, i.e., the set of elements in `G` that `f` maps to `1`. More concisely: For any monoid homomorphism `f : G → M` between a group `G` and a monoid `M` with identity, an element `x` in `G` is in the kernel of `f` if and only if `f(x) = 1`.
`Subgroup.NormalizerCondition.normal_of_coatom` theorem Subgroup.NormalizerCondition.normal_of_coatom : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), NormalizerCondition G → IsCoatom H → H.Normal In any group that meets the Normalizer Condition, this theorem states that any maximal subgroup is normal. The Normalizer Condition implies that every proper subgroup of a group is also a proper normal subgroup of the normalizer of that subgroup within the group. In this context, a maximal subgroup is considered a coatom, defined as a subgroup that has no other subgroups between it and the top element, and is not the top element itself. Therefore, if a group satisfies the Normalizer Condition, any such coatom, or maximal subgroup, is also normal. More concisely: In groups satisfying the Normalizer Condition, maximal subgroups are normal.
`MonoidHom.comap_bot` theorem MonoidHom.comap_bot : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N), Subgroup.comap f ⊥ = f.ker := by sorry This theorem states that for any given monoid homomorphism `f` from a group `G` to another group `N`, the preimage of the trivial subgroup in `N` under `f` (i.e., the set of elements in `G` that are mapped to the identity element in `N` by `f`) is equal to the kernel of `f`. In other words, the set of elements in `G` that are sent to the identity element in `N` by the homomorphism `f` forms a subgroup of `G`, and this subgroup is the kernel of `f`. More concisely: The preimage of the identity element under a group homomorphism is equal to the kernel of the homomorphism.
`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.1` theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.1 : ∀ {S : Type u_5} {G : Type u_6} [inst : InvolutiveInv G] {x : SetLike S G} [inst_1 : InvMemClass S G] {H : S} {x_1 : G}, (x_1⁻¹ ∈ H) = (x_1 ∈ H) The theorem states that for any types `S` and `G`, given that `G` has an involution, and `S` is a set-like structure over `G` that supports membership operation, for any element `H` of `S` and any element `x_1` of `G`, `x_1` being an element of `H` is equivalent to its inverse `x_1⁻¹` being an element of `H`. In other words, in the context of a group with involutive inversion, an element is in a subgroup if and only if its inverse is also in the subgroup. More concisely: In a group with involutive inversion, an element is in a subset if and only if its inverse is in the subset.
`AddSubgroup.eq_bot_iff_forall` theorem AddSubgroup.eq_bot_iff_forall : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H = ⊥ ↔ ∀ x ∈ H, x = 0 This theorem states that for any given additive subgroup `H` of an additive group `G`, `H` is identical to the trivial group (denoted as `⊥`) if and only if all elements `x` in `H` are the zero element of the group. In other words, an additive subgroup is the trivial group if every element in it is zero. More concisely: An additive subgroup of a group is the trivial subgroup if and only if every element in it is the additive identity.
`AddSubgroup.sub_mem` theorem AddSubgroup.sub_mem : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) {x y : G}, x ∈ H → y ∈ H → x - y ∈ H This theorem states that an additive subgroup (`AddSubgroup`) is closed under subtraction. Specifically, for any type `G` that forms an additive group, and any `AddSubgroup` `H` of this `G`, if `x` and `y` are elements of `H`, then the result of subtracting `y` from `x` (denoted as `x - y`) is also an element of `H`. Here, closed under subtraction means that subtraction of any two elements in the subgroup will always result in another element within the same subgroup. More concisely: For any additive subgroup `H` of an additive group `G`, if `x, y ∈ H`, then `x - y ∈ H`.
`Mathlib.GroupTheory.Subgroup.Basic._auxAddLemma.43` theorem Mathlib.GroupTheory.Subgroup.Basic._auxAddLemma.43 : ∀ {b a : Prop}, (∃ (_ : a), b) = (a ∧ b) This theorem states that for any two propositions `a` and `b`, the existence of `b` given `a` is equivalent to the conjunction of `a` and `b`. In other words, it asserts that 'there exists `b` such that `a` is true' is logically the same as 'both `a` and `b` are true'. More concisely: The theorem asserts that for all propositions `a` and `b`, `(∃ (x : Prop), b) ↔ (a ∧ b)`.
`AddSubgroup.Normal.mem_comm_iff` theorem AddSubgroup.Normal.mem_comm_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.Normal → ∀ {a b : G}, a + b ∈ H ↔ b + a ∈ H This theorem states that for any additive group `G`, any additive subgroup `H` of `G`, and any two elements `a` and `b` of `G`, if `H` is a normal subgroup (under addition), then `a + b` is in `H` if and only if `b + a` is in `H`. Essentially, this theorem is saying that if `H` is a normal subgroup, then the order in which you add two group elements doesn't matter for membership in `H`. More concisely: If `H` is a normal subgroup of an additive group `G`, then for all `a, b` in `G`, `a + b` is in `H` if and only if `b + a` is in `H`.
`Subgroup.Normal.comap` theorem Subgroup.Normal.comap : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {H : Subgroup N}, H.Normal → ∀ (f : G →* N), (Subgroup.comap f H).Normal The theorem `Subgroup.Normal.comap` states that for any groups `G` and `N`, any subgroup `H` of `N`, and any monoid homomorphism `f` from `G` to `N`, if the subgroup `H` is normal, then the preimage of `H` along `f` is also a normal subgroup of `G`. The preimage of a subgroup along a monoid homomorphism is defined by the function `Subgroup.comap`. In mathematical terms, if `H` is a normal subgroup of `N` and `f: G -> N` is a homomorphism, then `f^-1(H)`, the preimage of `H` under `f`, is a normal subgroup of `G`. More concisely: If `H` is a normal subgroup of group `N` and `f` is a homomorphism from group `G` to `N`, then the preimage `f^-1(H)` is a normal subgroup of `G`.
`MonoidHom.range_top_iff_surjective` theorem MonoidHom.range_top_iff_surjective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_7} [inst_1 : Group N] {f : G →* N}, f.range = ⊤ ↔ Function.Surjective ⇑f This theorem states that for any given groups `G` and `N`, and any monoid homomorphism `f` from `G` to `N`, the range of `f` is equal to the entire group `N` (denoted by `⊤`) if and only if `f` is a surjective function. In other words, a monoid homomorphism from one group to another is surjective (every element in the target group is the image of some element in the source group) if and only if its range covers the entire target group. More concisely: A monoid homomorphism between groups is surjective if and only if its image equals the entire target group.
`Subgroup.eq_bot_iff_forall` theorem Subgroup.eq_bot_iff_forall : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H = ⊥ ↔ ∀ x ∈ H, x = 1 := by sorry This theorem states that for any type `G` equipped with a group structure, and for any subgroup `H` of `G`, the subgroup `H` is equal to the trivial subgroup (denoted by `⊥`) if and only if all elements `x` in `H` are equal to the identity element (denoted by `1`). In other words, this theorem provides a characterization of trivial subgroups: a subgroup is trivial if and only if it only contains the identity element. More concisely: A subgroup of a group is trivial if and only if it consists only of the identity element.
`AddSubgroup.coe_top` theorem AddSubgroup.coe_top : ∀ {G : Type u_1} [inst : AddGroup G], ↑⊤ = Set.univ This theorem is stating that for any type `G` that has an additive group structure, the set of all elements of the additive group (represented by `↑⊤`) is equal to the universal set of the type `G` (represented by `Set.univ`). In other words, every element of the type `G` is an element of the additive group. Here, `⊤` stands for the top element in the lattice of subgroups, i.e., the entire group itself. More concisely: For any additive group `G`, the set of all group elements is equal to the universal set of `G`. In symbols, `↑⊤ = Set.univ` for the additive group `G`.
`AddSubgroup.closure_mono` theorem AddSubgroup.closure_mono : ∀ {G : Type u_1} [inst : AddGroup G] ⦃h k : Set G⦄, h ⊆ k → AddSubgroup.closure h ≤ AddSubgroup.closure k := by sorry The theorem `AddSubgroup.closure_mono` asserts that the closure operation for additive subgroups over a set is monotone. In other words, for any type `G` that forms an addition group, if `h` and `k` are sets of `G` and `h` is a subset of `k`, then the additive subgroup generated by `h` (`AddSubgroup.closure h`) is a subgroup of (or equal to) the additive subgroup generated by `k` (`AddSubgroup.closure k`). This express the intuitive notion that taking the closure of a larger set cannot result in a smaller subgroup. More concisely: For any additive group `G`, if `h` is a subset of `k` in `G`, then `AddSubgroup.closure h` is a subgroup of `AddSubgroup.closure k`.
`Subgroup.bot_or_nontrivial` theorem Subgroup.bot_or_nontrivial : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H = ⊥ ∨ Nontrivial ↥H := by sorry This theorem states that for any group `G` and a subgroup `H` of `G`, `H` is either the trivial subgroup or it is nontrivial. In other words, any given subgroup of a group is either the subgroup containing only the identity element (`⊥`) or it has two distinct elements, thereby being nontrivial. More concisely: Every subgroup of a group is either the trivial subgroup or nontrivial.
`Subgroup.mul_mem_cancel_right` theorem Subgroup.mul_mem_cancel_right : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) {x y : G}, x ∈ H → (y * x ∈ H ↔ y ∈ H) This theorem states that for any type `G` that has a group structure, given a subgroup `H` of `G` and any elements `x` and `y` of `G`, if `x` belongs to `H`, then `y * x` belongs to `H` if and only if `y` belongs to `H`. This means that multiplication with `x` from the right within the subgroup `H` has a cancellation property, i.e., the presence of `x` on the right side of the multiplication does not affect the membership of the result in the subgroup `H`. More concisely: For any group `G` and subgroup `H`, if `x` is in `H` and `y` is in `H`, then `y * x` is in `H`. (The theorem also states the converse that if `x` is in `H` and `y` is in `H` such that `y * x` is in `H`, then `y` is in `H`, but stating both parts together in a single sentence would make it more complex.)
`Subgroup.closure_induction` theorem Subgroup.closure_induction : ∀ {G : Type u_1} [inst : Group G] {k : Set G} {p : G → Prop} {x : G}, x ∈ Subgroup.closure k → (∀ x ∈ k, p x) → p 1 → (∀ (x y : G), p x → p y → p (x * y)) → (∀ (x : G), p x → p x⁻¹) → p x This theorem is an induction principle for membership in the closure of a set in a group. If a certain property `p` is satisfied by the identity element `1` and all elements of a set `k`, and `p` is also preserved under group multiplication and taking the inverse, then the property `p` holds for all elements in the closure of the set `k` in the group. In other words, if you start with a subset of elements that satisfy a rule, and that rule is preserved under the operations of the group, then the rule is satisfied by the smallest subgroup containing the subset. More concisely: If a property is satisfied by the identity element and all elements of a set in a group, and is preserved under group multiplication and taking inverses, then the property holds for all elements in the closure of the set in the group.
`AddSubgroup.map_equiv_eq_comap_symm` theorem AddSubgroup.map_equiv_eq_comap_symm : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G ≃+ N) (K : AddSubgroup G), AddSubgroup.map (↑f) K = AddSubgroup.comap (↑f.symm) K This theorem states that for any additive group isomorphism `f` from `G` to `N` and any additive subgroup `K` of `G`, the image of `K` under the isomorphism `f` is the same as the preimage of `K` under the inverse of the isomorphism `f`. This holds for any types `G` and `N` which have `AddGroup` instances. In other words, it establishes a correspondence between the subgroup `K` of the original group and the mapped group under the isomorphism and its inverse. More concisely: For any additive group isomorphism `f` and subgroup `K` of a group `G` with `AddGroup` instances, `f(K) = {f(x) \| x ∈ K} = {y \| ∃x. y = f(x) ∧ x ∈ K} = f⁻¹⁻¹(K)`.
`AddMonoidHom.map_closure` theorem AddMonoidHom.map_closure : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (s : Set G), AddSubgroup.map f (AddSubgroup.closure s) = AddSubgroup.closure (⇑f '' s) This theorem states that for any additive group `G`, any other additive group `N`, a homomorphism `f` from `G` to `N`, and a set `s` in `G`, the image under the homomorphism `f` of the additive subgroup generated by the set `s` is equal to the additive subgroup generated by the image of the set `s` under the homomorphism `f`. In other words, the process of mapping a subgroup via a homomorphism and thereafter generating a subgroup from a set commutes with the process of first generating a subgroup and then mapping it via the homomorphism. More concisely: For any additive groups G and N, homomorphism f, and set s in G, the subgroup generated by the images of s under f is equal to f(the subgroup generated by s).
`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.72` theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.72 : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {K : AddSubgroup G} {y : N}, (y ∈ AddSubgroup.map f K) = ∃ x ∈ K, f x = y This theorem states that for all additively grouped types `G` and `N`, a function `f` from `G` to `N` that preserves the group structure (`G →+ N`), a subgroup `K` of `G`, and an element `y` of `N`, `y` is in the image of the subgroup `K` under the function `f` if and only if there exists an element `x` in `K` such that `f(x) = y`. This image is itself a subgroup of `N` as defined by the `AddSubgroup.map` function. This is essentially the definition of the image of a set under a function in the context of additive groups and their subgroups. More concisely: For any additive group `G`, subgroup `K` of `G`, function `f : G -> N` preserving the group structure, and `y` in `N`, `y` is in the image of `K` under `f` if and only if there exists an `x` in `K` such that `f(x) = y`, and the image `f[K]` is a subgroup of `N`.
`mul_mem_cancel_left` theorem mul_mem_cancel_left : ∀ {G : Type u_1} [inst : Group G] {S : Type u_6} {H : S} [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G] {x y : G}, x ∈ H → (x * y ∈ H ↔ y ∈ H) This theorem, `mul_mem_cancel_left`, states that for any given type `G` that forms a group, a type `S`, an instance `H` of `S`, where `S` behaves like a set for `G` and `S` is a subgroup class of `G`, given any two elements `x` and `y` of the group `G`, if `x` is an element of `H`, then `x * y` is an element of `H` if and only if `y` is an element of `H`. In simpler terms, in the context of a given subgroup `H` of a group `G`, if we multiply an element of the subgroup by another element from the group, the result is in the subgroup if and only if the second element was already in the subgroup. More concisely: If `H` is a subgroup of a group `G`, then for all `x in H` and `y in G`, `x y` is in `H` if and only if `y` is in `H`.*
`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.70` theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.70 : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {K : AddSubgroup N} {f : G →+ N} {x : G}, (x ∈ AddSubgroup.comap f K) = (f x ∈ K) This theorem states that for any types `G` and `N` that are equipped with `AddGroup` structures, any subgroup `K` of `N`, any homomorphism `f` from `G` to `N`, and any element `x` of `G`, the element `x` is in the preimage of the subgroup `K` under the homomorphism `f` if and only if the image of `x` under `f` is in `K`. In simpler terms, `x` is in the preimage of `K` via `f` exactly when `f(x)` is in `K`. More concisely: For any AddGroup types G and N, homomorphism f : G -> N, subgroup K of N, and element x in G, x is in the preimage of K under f if and only if f(x) is in K.
`mul_mem_cancel_right` theorem mul_mem_cancel_right : ∀ {G : Type u_1} [inst : Group G] {S : Type u_6} {H : S} [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G] {x y : G}, x ∈ H → (y * x ∈ H ↔ y ∈ H) This theorem states that for any type `G` which is a group, and any subtype `S` of `G`, if `H` is of type `S` and both `S` and `G` have a `SubgroupClass`, then given two elements `x` and `y` from the group `G`, if `x` belongs to `H`, then `y * x` belongs to `H` if and only if `y` belongs to `H`. In mathematical terms, if `H` is a subgroup of a group and `x` is an element of `H`, then another element `y` times `x` is in `H` if and only if `y` is in `H`. More concisely: If `H` is a subgroup of group `G` and `x` is an element of `H`, then for all `y` in `G`, `y x` is in `H` if and only if `y` is in `H`.*
`AddSubgroup.addSubgroupOf_inj` theorem AddSubgroup.addSubgroupOf_inj : ∀ {G : Type u_1} [inst : AddGroup G] {H₁ H₂ K : AddSubgroup G}, H₁.addSubgroupOf K = H₂.addSubgroupOf K ↔ H₁ ⊓ K = H₂ ⊓ K This theorem states that for any additive group `G` and any subgroups `H₁`, `H₂`, and `K` from `G`, the function `AddSubgroup.addSubgroupOf` is injective if and only if the intersection of `H₁` and `K` is equal to the intersection of `H₂` and `K`. In other words, two subgroups `H₁` and `H₂` of a given group `G` are viewed identically from the perspective of another subgroup `K` (i.e., `AddSubgroup.addSubgroupOf H₁ K = AddSubgroup.addSubgroupOf H₂ K`) if and only if their intersections with `K` are the same (i.e., `H₁ ⊓ K = H₂ ⊓ K`). More concisely: The function `AddSubgroup.addSubgroupOf` from `AddSubgroup` is injective on subgroups of an additive group `G` if and only if the intersections of any two subgroups with a fixed subgroup `K` are equal.
`AddSubgroup.map_comap_eq` theorem AddSubgroup.map_comap_eq : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (H : AddSubgroup N), AddSubgroup.map f (AddSubgroup.comap f H) = f.range ⊓ H This theorem states that for any additive group homomorphism `f` from an additive group `G` to another additive group `N`, and for any additive subgroup `H` of `N`, the image under `f` of the preimage of `H` under `f` equals the intersection of the range of `f` and `H`. In simpler terms, if you start with a subgroup `H` of `N`, pull it back to `G` using `f`, push it forward again to `N` using `f`, you get exactly the elements of `H` that are in the image of `G` under `f`. More concisely: For any additive group homomorphism $f$ from group $G$ to group $N$ and any subgroup $H$ of $N$, the image of the preimage $f^{-1}(H)$ under $f$ equals the intersection of $H$ and the range of $f$.
`AddMonoidHom.coe_range` theorem AddMonoidHom.coe_range : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N), ↑f.range = Set.range ⇑f The theorem `AddMonoidHom.coe_range` states that for any `AddMonoidHom` `f` from an `AddGroup` `G` to another `AddGroup` `N`, the range of `f` when considered as an `AddSubgroup` of `N` (expressed as `AddMonoidHom.range f`) is the same as the set of all values in `N` that `f` can produce (expressed as `Set.range ⇑f`). In other words, the set of all possible outputs of the homomorphism `f` is the same whether we consider `f` as a function from `G` to `N` or as a function from `G` to the `AddSubgroup` of `N` generated by the image of `f`. More concisely: The range of an AddMonoidHom as an AddSubgroup of the target group is equal to the image of the homomorphism.
`AddMonoidHom.liftOfRightInverse_comp_apply` theorem AddMonoidHom.liftOfRightInverse_comp_apply : ∀ {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [inst : AddGroup G₁] [inst_1 : AddGroup G₂] [inst_2 : AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : { g // f.ker ≤ g.ker }) (x : G₁), ((f.liftOfRightInverse f_inv hf) g) (f x) = ↑g x The theorem `AddMonoidHom.liftOfRightInverse_comp_apply` states that for any three groups `G₁`, `G₂`, and `G₃` and a given additive monoid homomorphism `f: G₁ →+ G₂`, if we have a function `f_inv: G₂ → G₁` that is a right inverse to `f` (i.e., `f ∘ f_inv = id`), then for any homomorphism `g` whose kernel is a subset of the kernel of `f`, and for any element `x` of `G₁`, the composition of `f` with the lift of `g` with respect to `f_inv` and `hf` evaluated at `x` equals the evaluation of `g` at `x`. In other words, it says the lifted homomorphism behaves the same as the original homomorphism `g` on the image of `f`. More concisely: For additive monoid homomorphisms $f: G\_1 \to G\_2$ and given a right inverse $f\_{inv}: G\_2 \to G\_1$ such that $f \circ f\_{inv} = id\_{G\_2}$, if homomorphism $g: G\_1 \to G\_3$ has a kernel contained in $f$'s kernel, then $g(x) = (g \circ (f\_{inv} \circ f))(x)$ for all $x \in G\_1$.
`Subgroup.map_map` theorem Subgroup.map_map : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) {N : Type u_5} [inst_1 : Group N] {P : Type u_6} [inst_2 : Group P] (g : N →* P) (f : G →* N), Subgroup.map g (Subgroup.map f K) = Subgroup.map (g.comp f) K The theorem `Subgroup.map_map` states that for any two group homomorphisms `f` and `g` from groups `G` to `N` and `N` to `P` respectively, and any subgroup `K` of group `G`, the image of the subgroup `K` under the composition of `f` and `g` is the same as the image of the image of `K` under `f` under `g`. In mathematical terms, if you have two group homomorphisms `f: G → N` and `g: N → P`, and a subgroup `K` of `G`, then `g(f(K)) = (g ∘ f)(K)`. This theorem essentially asserts the compatibility of the map function with the composition of homomorphisms in the context of subgroups. More concisely: For any group homomorphisms f : G → N and g : N → P, and subgroup K of G, g(f(K)) = (g ∘ f)(K).
`Group.conj_mem_conjugatesOfSet` theorem Group.conj_mem_conjugatesOfSet : ∀ {G : Type u_1} [inst : Group G] {s : Set G} {x c : G}, x ∈ Group.conjugatesOfSet s → c * x * c⁻¹ ∈ Group.conjugatesOfSet s The theorem `Group.conj_mem_conjugatesOfSet` states that for any group `G`, given a set `s` of elements from `G` and any two elements `x` and `c` from `G`, if `x` is in the set of all conjugates of the elements of `s`, then the conjugate of `x` by `c` (expressed as `c * x * c⁻¹`) is also in the set of all conjugates of the elements of `s`. In other words, the set of all conjugates of a set in a group is closed under the operation of conjugation. More concisely: If `x` is in the set of conjugates of elements in `s` in a group `G`, then `c x * c⁻¹` is also in the set of conjugates of elements in `s`.*
`Subgroup.mul_mem_cancel_left` theorem Subgroup.mul_mem_cancel_left : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) {x y : G}, x ∈ H → (x * y ∈ H ↔ y ∈ H) This is a theorem about groups and subgroups in the field of algebra. It states that for any group `G` and any subgroup `H` of `G`, and for any elements `x` and `y` of `G`, if `x` is an element of `H`, then the multiplication of `x` and `y` (`x * y`) is in `H` if and only if `y` is in `H`. In other words, within a group, if a member of a subgroup multiplies with any element and the result is still in the subgroup, then the other element must also be a member of the subgroup. This theorem applies to all types `G` that have a group structure. More concisely: For any group `G` and subgroup `H`, if `x ∈ H` and `y ∈ H`, then `x y ∈ H`.*
`AddSubgroup.subset_closure` theorem AddSubgroup.subset_closure : ∀ {G : Type u_1} [inst : AddGroup G] {k : Set G}, k ⊆ ↑(AddSubgroup.closure k) This theorem states that, for any additive group `G` and any set `k` of elements of `G`, the set `k` is a subset of the additive subgroup generated by `k`. In simpler terms, this means that every element of the set `k` is also an element of the subgroup created by taking all possible sums (with repetition) of elements from `k`. More concisely: For any additive group G and subset k of its elements, k is contained in the additive subgroup generated by k.
`AddSubgroup.characteristic_iff_comap_le` theorem AddSubgroup.characteristic_iff_comap_le : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.Characteristic ↔ ∀ (ϕ : G ≃+ G), AddSubgroup.comap ϕ.toAddMonoidHom H ≤ H This theorem states that for any additive group `G` and any subgroup `H` of `G`, the subgroup `H` is said to be characteristic if and only if, for all additive equivalences `ϕ` from `G` to itself, the preimage of the subgroup `H` under the additive monoid homomorphism obtained from `ϕ` is a subset (or equal to) the subgroup `H`. In mathematical terms, a subgroup `H` of `G` is characteristic if and only if ∀ϕ : G ≃+ G, ϕ^(-1)(H) ⊆ H. More concisely: A subgroup H of an additive group G is characteristic if and only if the preimage of H under any additive group homomorphism from G to itself contains H.
`Subgroup.inv_mem` theorem Subgroup.inv_mem : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) {x : G}, x ∈ H → x⁻¹ ∈ H This theorem states that for any subgroup `H` of a group `G`, if an element `x` belongs to `H`, then the inverse of `x` (denoted as `x⁻¹`) also belongs to `H`. This is a property of subgroups in group theory, which states that subgroups are closed under the operation of taking inverses. In other words, every element in a subgroup has its inverse also in the same subgroup. More concisely: For any subgroup `H` of a group `G`, if `x` is an element of `H`, then `x⁻¹` (the inverse of `x`) is also an element of `H`.
`AddMonoidHom.comap_bot` theorem AddMonoidHom.comap_bot : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N), AddSubgroup.comap f ⊥ = f.ker The theorem `AddMonoidHom.comap_bot` states that for any additive group homomorphism `f` from an additive group `G` to another additive group `N`, the preimage of the bottom (trivial) subgroup under `f` is the kernel of `f`. In other words, the set of all elements in `G` that `f` maps to the identity element in `N` (which is the definition of the kernel of `f`) is the same as the set of all elements in `G` that get mapped to elements in the trivial subgroup of `N` under `f`. More concisely: The preimage of the trivial subgroup under an additive group homomorphism is equal to the kernel of the homomorphism.
`Subgroup.normalClosure_le_normal` theorem Subgroup.normalClosure_le_normal : ∀ {G : Type u_1} [inst : Group G] {s : Set G} {N : Subgroup G} [inst_1 : N.Normal], s ⊆ ↑N → Subgroup.normalClosure s ≤ N The theorem `Subgroup.normalClosure_le_normal` states that for any type `G` that forms a group, any set `s` of elements of `G`, and any normal subgroup `N` of `G`, if `s` is a subset of `N` then the normal closure of `s` is a subgroup of, or equal to, `N`. In other words, the smallest normal subgroup that contains `s` is contained within any other normal subgroup that contains `s`. This is a property of the normal closure operation in group theory. More concisely: For any group G, normal subgroup N, and subset s of G, if s is contained in N and the normal closure of s is defined, then the normal closure of s is a subgroup of N.
`AddSubgroup.map_equiv_eq_comap_symm'` theorem AddSubgroup.map_equiv_eq_comap_symm' : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G ≃+ N) (K : AddSubgroup G), AddSubgroup.map f.toAddMonoidHom K = AddSubgroup.comap f.symm.toAddMonoidHom K The theorem `AddSubgroup.map_equiv_eq_comap_symm'` asserts that for every additive group isomorphism `f` from an additive group `G` to another additive group `N`, and for any additive subgroup `K` of `G`, the image of `K` under `f` is the same as the preimage of `K` under the inverse of `f`. In other words, applying `f` to `K` yields the same result as applying the inverse of `f` to `K` in the opposite group direction. More concisely: For every additive group isomorphism $f$ from an additive group $G$ to an additive group $N$, and for any additive subgroup $K$ of $G$, $f(K) = N[f^{-1}(K)]$.
`AddMonoidHom.mem_ker` theorem AddMonoidHom.mem_ker : ∀ {G : Type u_1} [inst : AddGroup G] {M : Type u_7} [inst_1 : AddZeroClass M] (f : G →+ M) {x : G}, x ∈ f.ker ↔ f x = 0 The theorem `AddMonoidHom.mem_ker` states that for any `AddGroup` G, any `AddZeroClass` M, and any additive monoid homomorphism `f` from G to M, an element `x` from G belongs to the kernel of `f` if and only if the result of applying `f` to `x` is 0. The kernel of the homomorphism `f` is defined as the subgroup of elements from G that, when mapped by `f`, result in the additive identity in M. More concisely: For any additive monoid homomorphism from an add group to an additive semigroup with additive identity, an element in the domain maps to the additive identity in the codomain if and only if it belongs to the kernel of the homomorphism.
`NegMemClass.coe_neg` theorem NegMemClass.coe_neg : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_6} {H : S} [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G] (x : ↥H), ↑(-x) = -↑x This theorem states that for any type `G` that has an `AddGroup` structure, any type `S`, any `H` of type `S` that has a `SetLike` structure and is an `AddSubgroupClass` of `G`, and any element `x` from `H`, the inverse of `x` in `H` is equal to the inverse of the coerced `x` in `G`. In mathematical terms, this means that if `H` is a subgroup of an additive group `G`, then the negation of an element in `H` is the same as the negation of that element in `G` when both are considered in the context of `G`. More concisely: For any additive group `G`, subgroup `H` of `G` with `AddSubgroupClass` structure, and element `x` in `H`, the negation of `x` in `H` equals the negation of `x` in `G` as elements of `G`.
`AddSubgroup.coe_zero` theorem AddSubgroup.coe_zero : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), ↑0 = 0 This theorem states that for any given additive subgroup `H` of a given type `G` (where `G` is an additive group), the additive identity (zero) in the additive group `G` is the same as the additive identity in the underlying set of `H`. In mathematical terms, this means that for any additive subgroup `H` of an additive group `G`, the identity element 0 of `G` is the same as the identity element 0 of `H` when `H` is considered as a subset of `G`. More concisely: The additive identity of an additive subgroup is the same as the additive identity of its underlying set in an additive group.
`Subgroup.closure_induction'` theorem Subgroup.closure_induction' : ∀ {G : Type u_1} [inst : Group G] {k : Set G} {p : (x : G) → x ∈ Subgroup.closure k → Prop}, (∀ (x : G) (h : x ∈ k), p x ⋯) → p 1 ⋯ → (∀ (x : G) (hx : x ∈ Subgroup.closure k) (y : G) (hy : y ∈ Subgroup.closure k), p x hx → p y hy → p (x * y) ⋯) → (∀ (x : G) (hx : x ∈ Subgroup.closure k), p x hx → p x⁻¹ ⋯) → ∀ {x : G} (hx : x ∈ Subgroup.closure k), p x hx This theorem, named `Subgroup.closure_induction'`, is a dependent version of `Subgroup.closure_induction`. Consider a type `G` with a group structure, a set `k` of elements of `G`, and a predicate `p` that applies to elements of the closure of `k` under the group operation. This theorem states that if the following conditions hold: 1. The predicate `p` holds for every element in the set `k`. 2. The predicate `p` holds for the identity element of the group. 3. For any two elements `x` and `y` in the closure of `k`, if `p` holds for `x` and `y`, then `p` also holds for the product `x * y`. 4. For any element `x` in the closure of `k`, if `p` holds for `x`, then `p` also holds for the inverse `x⁻¹`. Then the predicate `p` holds for every element in the closure of `k`. This is a form of structural induction for subgroups generated by a set, asserting that a property verified for the generating set and preserved under the group operations, holds for the entire subgroup. More concisely: If `k` is a set of elements in a group `G` such that `p` holds for every element in `k` and the identity element, and `p` is closed under group multiplication and taking inverses in the closure of `k`, then `p` holds for every element in the subgroup generated by `k`.
`AddSubgroup.le_normalizer_map` theorem AddSubgroup.le_normalizer_map : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N), AddSubgroup.map f H.normalizer ≤ (AddSubgroup.map f H).normalizer This theorem states that for any two types `G` and `N` that are equipped with `AddGroup` structures, for any additive subgroup `H` of `G`, and for any additive monoid homomorphism `f` from `G` to `N`, the image of the normalizer of `H` under `f` is contained within the normalizer of the image of `H` under `f`. Here, the normalizer of a subgroup is the set of all elements that commute with every element of the subgroup. This theorem is essentially comparing the normalizing behaviours before and after the mapping `f`. More concisely: For any additive groups `G` and `N`, any additive subgroup `H` of `G`, and any additive monoid homomorphism `f` from `G` to `N`, the normalizer of `H` in `G` is contained in the normalizer of `f(H)` in `N`.
`Subgroup.map_eq_bot_iff` theorem Subgroup.map_eq_bot_iff : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H : Subgroup G) {f : G →* N}, Subgroup.map f H = ⊥ ↔ H ≤ f.ker This theorem states that for any group `G`, any group `N`, a subgroup `H` of `G`, and a monoid homomorphism `f` from `G` to `N`, the image of the subgroup `H` under the homomorphism `f` is the trivial subgroup (denoted by `⊥`) if and only if `H` is a subset of the kernel of the homomorphism `f`. Here, the kernel of a homomorphism `f` is defined as the subgroup of elements `x` in `G` such that `f(x)` equals the identity element in `N`. More concisely: A subgroup H of a group G is mapped to the trivial subgroup under a group homomorphism f to N if and only if H is contained in the kernel of f.
`MonoidHom.map_closure` theorem MonoidHom.map_closure : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) (s : Set G), Subgroup.map f (Subgroup.closure s) = Subgroup.closure (⇑f '' s) The theorem `MonoidHom.map_closure` states that for any two groups `G` and `N`, and a monoid homomorphism `f` from `G` to `N`, the image under the homomorphism `f` of the subgroup generated by a set `s` in `G` is equal to the subgroup generated by the image of the set `s` under `f` in `N`. In other words, if you have a subgroup generated by a set in one group and you map that subgroup through a group homomorphism, you get the same result as if you first mapped the original set through the homomorphism and then generated a subgroup in the target group. This theorem captures an important property of group homomorphisms and their interaction with the operation of taking the subgroup generated by a set. More concisely: For any group homomorphism between groups G and N, and any subset s of G, the image under the homomorphism of the subgroup generated by s in G is equal to the subgroup generated by the image of s in N.
`Subgroup.subgroupOf_self` theorem Subgroup.subgroupOf_self : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.subgroupOf H = ⊤ This theorem states that, for any group `G` and subgroup `H` of `G`, the subgroup of `H` viewed as a subgroup of itself (`H`), using the `Subgroup.subgroupOf` function, is the top subgroup (i.e., the whole group `H`). In other words, the intersection of a subgroup with itself is the subgroup itself. More concisely: For any subgroup `H` of a group `G`, `H.subgroupOf H` equals `H`.
`Subgroup.mul_mem` theorem Subgroup.mul_mem : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) {x y : G}, x ∈ H → y ∈ H → x * y ∈ H := by sorry This theorem states that a subgroup is closed under multiplication. Specifically, in the context of a group `G`, if `H` is a subgroup of `G`, and `x` and `y` are elements of `H`, then the product of `x` and `y` is also an element of `H`. This property is essential to the definition of a subgroup in group theory. More concisely: If `H` is a subgroup of group `G`, then for all `x, y ∈ H`, their product `x y` is also an element of `H`.*
`Subgroup.map_id` theorem Subgroup.map_id : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G), Subgroup.map (MonoidHom.id G) K = K := by sorry The theorem `Subgroup.map_id` states that for any given group `G` and any subgroup `K` of `G`, if we apply the identity map of the monoid `G` to `K` using the function `Subgroup.map`, the result is `K` itself. In simple terms, the image of a subgroup under the identity map is the subgroup itself. More concisely: For any group (G, ) and subgroup K of G, Subgroup.map G id K = K.*
`Subgroup.le_normalizer_comap` theorem Subgroup.le_normalizer_comap : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {N : Type u_5} [inst_1 : Group N] (f : N →* G), Subgroup.comap f H.normalizer ≤ (Subgroup.comap f H).normalizer This theorem states that for any group `G`, subgroup `H` of `G`, group `N`, and monoid homomorphism `f` from `N` to `G`, the preimage of the normalizer of `H` under the map `f` is contained in the normalizer of the preimage of `H` under the map `f`. In other words, if we first take the normalizer of `H` in `G` and then take the preimage under `f`, we get a subgroup of `N` that is contained in the subgroup we get if we first take the preimage of `H` under `f` and then take the normalizer in `N`. More concisely: For any group `G`, subgroup `H` of `G`, monoid `N`, and group homomorphism `f` from `N` to `G`, the normalizer of `f''(N)` in `G` contains `f''(N'_H)`, where `N'_H` is the normalizer of `H` in `N`.
`Subgroup.commute_of_normal_of_disjoint` theorem Subgroup.commute_of_normal_of_disjoint : ∀ {G : Type u_1} [inst : Group G] (H₁ H₂ : Subgroup G), H₁.Normal → H₂.Normal → Disjoint H₁ H₂ → ∀ (x y : G), x ∈ H₁ → y ∈ H₂ → Commute x y The theorem `Subgroup.commute_of_normal_of_disjoint` states that for any type `G` that has an associated group structure, given two subgroups `H₁` and `H₂` of `G` such that `H₁` and `H₂` are normal and disjoint, any element `x` from `H₁` and any element `y` from `H₂` commute. In other words, if `x` is in `H₁` and `y` is in `H₂`, then the multiplication of `x` and `y` is the same as the multiplication of `y` and `x`. This can be expressed in mathematical terms as: for all `x` in `H₁` and `y` in `H₂`, `x * y = y * x`. More concisely: For any group `G` and normal and disjoint subgroups `H₁` and `H₂` of `G`, any `x` in `H₁` and `y` in `H₂` commute, i.e., `x y = y * x`.*
`AddSubgroup.add_mem_cancel_left` theorem AddSubgroup.add_mem_cancel_left : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) {x y : G}, x ∈ H → (x + y ∈ H ↔ y ∈ H) This theorem states that for any additive group `G` and any subgroup `H` of `G`, if an element `x` belongs to `H`, then another element `y` belongs to `H` if and only if the result of adding `x` to `y` also belongs to `H`. This is essentially saying that in an additive group, if a particular element is in a subgroup, then adding that element to another does not change the membership status of the second element in the subgroup. More concisely: For any additive group G and subgroup H, if x is in H and y belongs to G, then x + y is in H if and only if y is in H.
`AddSubgroup.comap_map_eq` theorem AddSubgroup.comap_map_eq : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (H : AddSubgroup G), AddSubgroup.comap f (AddSubgroup.map f H) = H ⊔ f.ker The theorem `AddSubgroup.comap_map_eq` states that for any additive group homomorphism `f` from an additive group `G` to another additive group `N`, and for any additive subgroup `H` of `G`, the preimage of the image of the subgroup `H` under the map `f` is equal to the join (i.e., smallest superset) of the subgroup `H` and the kernel of the homomorphism `f`. In mathematical notation, this translates to `f⁻¹(f(H)) = H ∪ ker(f)`. This essentially means that any element in the preimage of the image of `H` is either in `H` or gets mapped to the additive identity in `N` by `f`. More concisely: The preimage of the image of a subgroup under an additive group homomorphism equals the subgroup's join with the homomorphism's kernel.
`SubgroupClass.coe_inv` theorem SubgroupClass.coe_inv : ∀ {G : Type u_1} [inst : Group G] {S : Type u_6} {H : S} [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G] (x : ↥H), ↑x⁻¹ = (↑x)⁻¹ This theorem, `SubgroupClass.coe_inv`, states that for any given group `G` of some type `u_1`, and any set `S` of type `u_6` that is a subgroup of `G`, the inverse of an element `x` in this subgroup `S` exists. Moreover, the theorem states that the inverse of the co-domain of `x` is equal to the co-domain of the inverse of `x`. In other words, taking the inverse before or after mapping `x` to the larger group `G` gives the same result. More concisely: For any group `G` and subgroup `S` of `G`, every element `x` in `S` has an inverse in `S`, and the inverse of `x` in `G` is the same as the inverse of the image of `x` in `G`.
`AddSubgroup.neg_mem'` theorem AddSubgroup.neg_mem' : ∀ {G : Type u_5} [inst : AddGroup G] (self : AddSubgroup G) {x : G}, x ∈ self.carrier → -x ∈ self.carrier := by sorry This theorem states that for any given additive subgroup (`self`) of an additive group `G`, if a certain element `x` belongs to this subgroup, then its negation `-x` also belongs to the same subgroup. In other words, the additive subgroup is closed under the operation of negation. More concisely: If `self` is an additive subgroup of an additive group `G`, then for all `x ∈ self`, it follows that `-x ∈ self`.
`AddSubgroup.map_equiv_normalizer_eq` theorem AddSubgroup.map_equiv_normalizer_eq : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H : AddSubgroup G) (f : G ≃+ N), AddSubgroup.map f.toAddMonoidHom H.normalizer = (AddSubgroup.map f.toAddMonoidHom H).normalizer The theorem states that for any additive group `G`, any additive group `N`, any additive subgroup `H` of `G`, and any additive group isomorphism `f` from `G` to `N`, the image of the `normalizer` of `H` under `f` is equal to the `normalizer` of the image of `H` under `f`. Here `normalizer` refers to the set of all elements in `G` that normalize `H`, i.e., the set of all `g` in `G` such that `g` multiplied by `h` multiplied by the inverse of `g` is in `H` for all `h` in `H`. The image of a set under `f` is defined to be the set of all `f(g)` for `g` in the set. The theorem thus relates the structure of the `normalizer` in the original group `G` and in its image group `N`. More concisely: For any additive groups G, N, subgroup H of G, and additive group isomorphism f from G to N, the normalizer of H in G maps to the normalizer of the image of H under f.
`Subgroup.subgroupOf_inj` theorem Subgroup.subgroupOf_inj : ∀ {G : Type u_1} [inst : Group G] {H₁ H₂ K : Subgroup G}, H₁.subgroupOf K = H₂.subgroupOf K ↔ H₁ ⊓ K = H₂ ⊓ K := by sorry This theorem states that for any type 'G' with group structure, and for any subgroups 'H₁', 'H₂' and 'K' of 'G', the injection of 'H₁' into 'K' is the same as the injection of 'H₂' into 'K' if and only if the intersection of 'H₁' and 'K' is equal to the intersection of 'H₂' and 'K'. In other words, it says that two subgroups are mapped to the same subgroup of 'K' by the function 'Subgroup.subgroupOf', precisely when their intersections with 'K' are the same. More concisely: For any groups G, subgroups H1, H2, and K, the injection of H1 into K equals the injection of H2 into K if and only if the intersections H1 ∩ K and H2 ∩ K are equal.
`AddSubgroup.map_comap_eq_self` theorem AddSubgroup.map_comap_eq_self : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {H : AddSubgroup N}, H ≤ f.range → AddSubgroup.map f (AddSubgroup.comap f H) = H The theorem `AddSubgroup.map_comap_eq_self` states that for every additive group homomorphism `f` from an additive group `G` to another additive group `N`, and for any additive subgroup `H` of `N`, if `H` is a subset of the range of `f`, then the image under `f` of the preimage of `H` under `f` is the same as `H` itself. Mathematically, this can be expressed as: if $H \subseteq \text{range}(f)$, then $f(f^{-1}(H)) = H$. This illustrates one of the fundamental properties of functions and their inverses when dealing with sets and subsets: the process of mapping a set through a function and then its inverse (or vice versa) results in the original set when the initial set is within the function's range. More concisely: If `H` is an additive subgroup of an additive group `N` contained in the image of an additive group homomorphism `f` from an additive group `G` to `N`, then `f(f⁻¹(H)) = H`.
`MonoidHom.coe_range` theorem MonoidHom.coe_range : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N), ↑f.range = Set.range ⇑f := by sorry The theorem `MonoidHom.coe_range` states that for any given monoid homomorphism `f` from a group `G` to a group `N`, the range of `f` when treated as a subgroup of `N` is equal to the set of all outputs of `f`. More formally, the set obtained by applying the monoid homomorphism `f` to all elements of the group `G` is exactly the same as the set of all possible outcomes of `f`. More concisely: The range of a group homomorphism as a subgroup of the target group is equal to the image of the homomorphism.
`Subgroup.map_le_iff_le_comap` theorem Subgroup.map_le_iff_le_comap : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {K : Subgroup G} {H : Subgroup N}, Subgroup.map f K ≤ H ↔ K ≤ Subgroup.comap f H The theorem `Subgroup.map_le_iff_le_comap` states that for any groups `G` and `N`, and any monoid homomorphism `f` from `G` to `N`, and for any subgroups `K` of `G` and `H` of `N`, the image of `K` under `f` is a subgroup of `H` if and only if `K` is a subgroup of the preimage of `H` under `f`. This is a fundamental result about the relationship between the image and the preimage of a subgroup under a monoid homomorphism in the context of group theory. More concisely: For any groups G and N, monoid homomorphism f from G to N, and subgroups K of G and H of N, the image of K under f is a subgroup of H if and only if K is a subgroup of the preimage of H under f.
`AddMonoidHom.eqOn_closure` theorem AddMonoidHom.eqOn_closure : ∀ {G : Type u_1} [inst : AddGroup G] {M : Type u_7} [inst_1 : AddMonoid M] {f g : G →+ M} {s : Set G}, Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(AddSubgroup.closure s) This theorem states that if two additive monoid homomorphisms are equal on a set, then they remain equal on the closure of that set under the operation of an additive subgroup. In other words, if for every element in a set, two homomorphisms produce the same result, then this property will hold true for all elements in the additive subgroup generated by this set. Here, `G` is the type of elements in the given set which forms an additive group, `M` is the type of elements in the codomain of the homomorphisms which forms an additive monoid, `f` and `g` are the two additive monoid homomorphisms, and `s` is the original set. More concisely: If two additive monoid homomorphisms agree on a set, they agree on its additive subgroup closure.
`AddSubgroup.ext` theorem AddSubgroup.ext : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, (∀ (x : G), x ∈ H ↔ x ∈ K) → H = K This theorem states that two additive subgroups of a given additive group are equal if and only if they contain the same elements. In other words, for any type `G` equipped with an additive group structure and any two additive subgroups `H` and `K` of `G`, if every element `x` in `G` satisfies the condition that `x` is in `H` if and only if `x` is in `K`, then `H` and `K` are equal as subgroups. More concisely: Two additive subgroups of an additive group are equal if and only if they have the same elements.
`AddSubgroup.bot_or_exists_ne_zero` theorem AddSubgroup.bot_or_exists_ne_zero : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H = ⊥ ∨ ∃ x ∈ H, x ≠ 0 This theorem states that for any given additive group `G` and a subgroup `H` of `G`, `H` is either the trivial subgroup (represented as `⊥`, which consists only of the identity element, here `0`), or there exists an element `x` in `H` that is not equal to zero. In other words, every subgroup of an additive group is either trivial or includes a non-zero element. More concisely: Every subgroup of an additive group contains the trivial subgroup or a non-zero element.
`Subgroup.mem_top` theorem Subgroup.mem_top : ∀ {G : Type u_1} [inst : Group G] (x : G), x ∈ ⊤ This theorem states that for any given type `G` and any instance of a group `G`, every element `x` of `G` belongs to the top subgroup `⊤`. In the context of group theory, the top (or trivial) subgroup of a group is the group itself, hence every element of the group is a member of this subgroup. The theorem is universal, meaning it applies to all elements of all groups. More concisely: For any group `G` and all `x` in `G`, `x` belongs to the group `⊤` (i.e., `x ∈ ⊤`).
`AddSubgroup.ker_le_comap` theorem AddSubgroup.ker_le_comap : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (H : AddSubgroup N), f.ker ≤ AddSubgroup.comap f H This theorem states that for any additive group homomorphism `f` from an additive group `G` to another additive group `N`, and any additive subgroup `H` of `N`, the additive kernel of `f` is a subgroup of the preimage of `H` under `f`. In other words, all elements of `G` that are mapped to `0` in `N` by `f` (the kernel of `f`) are included in the set of elements of `G` that are mapped to `H` in `N` by `f` (the preimage of `H` under `f`). More concisely: The kernel of an additive group homomorphism is a subgroup of its preimage under that homomorphism.
`AddSubgroup.inclusion_injective` theorem AddSubgroup.inclusion_injective : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} (h : H ≤ K), Function.Injective ⇑(AddSubgroup.inclusion h) The theorem `AddSubgroup.inclusion_injective` states that for any type `G` that forms an additive group, and any additive subgroups `H` and `K` of `G` such that `H` is contained in `K`, the inclusion homomorphism from `H` to `K` is injective. In other words, if we have two elements in `H` that are mapped to the same element in `K` by the inclusion homomorphism, then those two elements were actually the same to start with. More concisely: If `H` is an additive subgroup of an additive group `G` with `H` contained in `K`, then the inclusion homomorphism from `H` to `K` is injective.
`Subgroup.mem_closure_singleton` theorem Subgroup.mem_closure_singleton : ∀ {G : Type u_1} [inst : Group G] {x y : G}, y ∈ Subgroup.closure {x} ↔ ∃ n, x ^ n = y This theorem states that for any group `G` and any two elements `x` and `y` in `G`, `y` belongs to the `Subgroup` generated by `{x}` if and only if there exists an integer `n` such that `x` to the power of `n` equals `y`. In other words, the theorem describes a property of the `Subgroup` generated by a single element: it consists of all integer powers of that element. More concisely: The Subgroup generated by an element x in a group G equals the set of all integer powers of x.
`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.36` theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.36 : ∀ {G : Type u_1} [inst : Group G] {x : G}, (x ∈ ⊥) = (x = 1) This theorem states that for any type `G` that has a group structure, and any element `x` of `G`, `x` belongs to the trivial subgroup (denoted by `⊥` in this context) if and only if `x` equals the identity element of the group (`1` in this context). In mathematical terms, it is saying that the trivial subgroup of a group is exactly the set containing just the identity element. More concisely: The trivial subgroup of a group is equal to the set of its identity element.
`inv_mem_iff` theorem inv_mem_iff : ∀ {S : Type u_5} {G : Type u_6} [inst : InvolutiveInv G] {x : SetLike S G} [inst_1 : InvMemClass S G] {H : S} {x_1 : G}, x_1⁻¹ ∈ H ↔ x_1 ∈ H This theorem, `inv_mem_iff`, states that for any set `H` of type `S`, which has the properties defined by an `InvMemClass` between `S` and `G`, and for any element `x_1` of type `G`, the inverse of `x_1` (denoted `x_1⁻¹`) is in `H` if and only if `x_1` itself is in `H`. Here `G` is a type with an involutive inverse operation, which means taking the inverse twice gives back the original element. More concisely: For any set `H` of type `S` defined by an `InvMemClass` between `S` and an involutive group `G`, and for all `x_1` in `G`, `x_1` is in `H` if and only if `x_1⁻¹` is in `H`.
`AddSubgroup.comap_normalizer_eq_of_surjective` theorem AddSubgroup.comap_normalizer_eq_of_surjective : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H : AddSubgroup G) {f : N →+ G}, Function.Surjective ⇑f → AddSubgroup.comap f H.normalizer = (AddSubgroup.comap f H).normalizer The theorem `AddSubgroup.comap_normalizer_eq_of_surjective` states that for any two types `G` and `N` with `AddGroup` structures, a subgroup `H` of `G`, and a surjective additive group homomorphism `f` from `N` to `G`, the preimage under `f` of the normalizer of `H` is equal to the normalizer of the preimage of `H` under `f`. In other words, if we have a surjective function from one additive group to another, the preimage of the set of elements that normalize a given subgroup in the target group is the same as the set of elements that normalize the preimage of the subgroup in the source group. More concisely: For any surjective additive group homomorphism between two additive groups and a subgroup of the domain, the preimage under the homomorphism of the normalizer of the subgroup is equal to the normalizer of the preimage of the subgroup.
`Subgroup.coe_mul` theorem Subgroup.coe_mul : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (x y : ↥H), ↑(x * y) = ↑x * ↑y This theorem is stating that, for any type `G` that has an instance of a group structure, and for any subgroup `H` of `G`, the multiplication of two elements `x` and `y` in `H` (viewed as elements of the larger group `G` through the injection `↑`) is the same as their multiplication within the subgroup. In other words, the process of lifting the subgroup elements to the larger group does not affect the result of the multiplication. More concisely: For any group `G` and subgroup `H`, and all `x, y ∈ H`, the multiplication `x y` in `G` agrees with the multiplication `x * y` within `H`.*
`AddSubgroup.zsmul_mem` theorem AddSubgroup.zsmul_mem : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) {x : G}, x ∈ K → ∀ (n : ℤ), n • x ∈ K This theorem states that for any additive group `G`, any subgroup `K` of `G`, and any element `x` of `G` that belongs to `K`, the result of the operation of integer multiplication `n • x` for any integer `n`, also belongs to `K`. In other words, the integer multiple of any element inside an additive subgroup remains within the same subgroup. More concisely: For any additive group G, subgroup K, and element x in K, the integer multiples of x belong to K.
`AddMonoidHom.rangeRestrict_surjective` theorem AddMonoidHom.rangeRestrict_surjective : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N), Function.Surjective ⇑f.rangeRestrict This theorem states that for any two types `G` and `N` that are additive groups, given a group homomorphism `f` from `G` to `N`, the function that restricts `f` to the range of `f` is surjective. In other words, for every element in the range of `f`, there exists an element in `G` such that applying the restricted function to this element gives the original element in the range. This means that the restricted function covers the entire range of `f`. More concisely: For any additive group homomorphism `f` from type `G` to type `N`, the restriction of `f` to the range of `f` is a surjection.
`Subgroup.coeSubtype` theorem Subgroup.coeSubtype : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), ⇑H.subtype = Subtype.val The theorem `Subgroup.coeSubtype` states that for any group `G` and any subgroup `H` of `G`, the function produced by `Subgroup.subtype H`, when applied to an element, is equivalent to retrieving the underlying element from the subtype with `Subtype.val`. This means that the natural group homomorphism from a subgroup `H` to group `G` simply extracts the underlying elements from the subgroup. More concisely: For any group `G` and subgroup `H`, the function `Subgroup.subtype H` is equal to the constant function that maps each element `x` in `H` to `x` itself.
`Subgroup.coe_map` theorem Subgroup.coe_map : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) (K : Subgroup G), ↑(Subgroup.map f K) = ⇑f '' ↑K This theorem states that for any two groups G and N, and a monoid homomorphism `f` from G to N, the image of a subgroup `K` of G under the mapping `f` is identical to the elements of the subgroup `K` mapped by `f`. In other words, applying the group homomorphism `f` to a subgroup `K` of `G` yields the same set of elements as applying `f` to each element of `K` individually. More concisely: For any group homomorphism `f` from group `G` to group `N` and any subgroup `K` of `G`, the image of `K` under `f` is equal to the set of elements in `N` obtained by applying `f` to every element in `K`.
`Subgroup.map_mono` theorem Subgroup.map_mono : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {K K' : Subgroup G}, K ≤ K' → Subgroup.map f K ≤ Subgroup.map f K' The theorem `Subgroup.map_mono` states that for any two subgroups `K` and `K'` of a group `G`, and a monoid homomorphism `f` from `G` to another group `N`, if `K` is a subset of `K'` (i.e., `K` is less than or equal to `K'`), then the image of `K` under `f` is also a subset of the image of `K'` under `f`. In other words, the mapping of subgroups through a monoid homomorphism preserves the subset relation. More concisely: If `K` is a subgroup of `K'` in a group `G` and `f` is a monoid homomorphism from `G` to a group `N`, then `f(K)` is a subgroup of `f(K')`.
`Subgroup.subtype_range` theorem Subgroup.subtype_range : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.subtype.range = H This theorem states that for any given group `G` and a subgroup `H` of `G`, the range of the natural group homomorphism from the subgroup `H` to the group `G` is the subgroup `H` itself. In other words, when we apply the `Subgroup.subtype` function to `H` and then calculate the `MonoidHom.range`, we get back the original subgroup `H`. More concisely: The natural homomorphism from a subgroup to a group maps the subgroup to itself.
`AddSubgroup.mem_bot` theorem AddSubgroup.mem_bot : ∀ {G : Type u_1} [inst : AddGroup G] {x : G}, x ∈ ⊥ ↔ x = 0 This theorem states that for any type `G` which has the structure of an additive group, an element `x` of `G` belongs to the trivial subgroup (denoted by `⊥`) if and only if `x` is the zero element of the group. In other words, the trivial subgroup of an additive group consists only of the zero element. More concisely: The trivial subgroup of an additive group is equal to the set of its zero elements.
`AddSubgroup.Normal.conj_mem` theorem AddSubgroup.Normal.conj_mem : ∀ {A : Type u_4} [inst : AddGroup A] {H : AddSubgroup A}, H.Normal → ∀ n ∈ H, ∀ (g : A), g + n + -g ∈ H This theorem states that for any additive group `A` and any normal subgroup `H` of `A`, if a number `n` belongs to the subgroup `H`, then the additive conjugate of `n` by any element `g` from `A` also belongs to `H`. In mathematical notation, for any `g` in `A` and any `n` in `H`, `g + n - g` always lies in `H`. This property is one of the defining characteristics of a normal subgroup in the context of group theory. More concisely: For any additive group `A`, normal subgroup `H`, and elements `g` in `A` and `n` in `H`, the additive conjugate `g + n - g` belongs to `H`.
`Subgroup.closure_union` theorem Subgroup.closure_union : ∀ {G : Type u_1} [inst : Group G] (s t : Set G), Subgroup.closure (s ∪ t) = Subgroup.closure s ⊔ Subgroup.closure t This theorem states that for any type `G` that has a group structure, given two sets `s` and `t` of elements of `G`, the subgroup generated by the union of `s` and `t` is equal to the join (supremum) of the subgroups generated by `s` and `t` respectively. In other words, the smallest subgroup of `G` that contains all elements of `s` and `t` is the smallest subgroup that includes both the smallest subgroup containing all elements of `s` and the smallest subgroup containing all elements of `t`. More concisely: For any group `G`, the subgroup generated by the union of two sets `s` and `t` in `G` is equal to the subgroup generated by the union of the subgroups generated by `s` and `t` separately.
`AddSubgroup.neg_mem_iff` theorem AddSubgroup.neg_mem_iff : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) {x : G}, -x ∈ H ↔ x ∈ H := by sorry This theorem states that for any given type `G` which has an addition group structure (`AddGroup G`), and for any addition subgroup `H` of `G`, an element `x` of `G` is in `H` if and only if the negation of `x` (denoted as `-x`) is also in `H`. In other words, it expresses the property of subgroups in an additive group where if `x` is an element of the subgroup, then its additive inverse `-x` is also an element of the subgroup, and vice versa. More concisely: For any additive group `G` and subgroup `H`, an element `x` in `G` belongs to `H` if and only if both `x` and `-x` belong to `H`.
`Subgroup.le_normalizer` theorem Subgroup.le_normalizer : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H ≤ H.normalizer This theorem states that, for any group `G` and any subgroup `H` of `G`, `H` is a sub-group of its normalizer. In other words, every element of `H` is also in the normalizer of `H`. This is because the normalizer of a subgroup is defined as the largest subgroup in which the given subgroup is normal. Hence, the given subgroup is always contained within its normalizer. More concisely: For any group `G` and subgroup `H` of `G`, `H` is a subgroup of its normalizer `N(H)` in `G`.
`Subgroup.comap_injective` theorem Subgroup.comap_injective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N}, Function.Surjective ⇑f → Function.Injective (Subgroup.comap f) The theorem `Subgroup.comap_injective` states that for all groups `G` and `N`, and for all monoid homomorphisms `f` from `G` to `N`, if `f` is a surjective function (that is, for every element in `N`, there exists an element in `G` such that the image of this element under `f` is that element in `N`), then the function `Subgroup.comap f` that maps subgroups of `N` to subgroups of `G` is injective (that is, if `Subgroup.comap f` maps two different subgroups of `N` to the same subgroup of `G`, then the two subgroups of `N` must have been the same to begin with). More concisely: If `f` is a surjective group homomorphism from `G` to `N`, then `Subgroup.comap f` is an injective function from the subgroup lattice of `N` to the subgroup lattice of `G`.
`AddSubgroup.closure_le` theorem AddSubgroup.closure_le : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) {k : Set G}, AddSubgroup.closure k ≤ K ↔ k ⊆ ↑K The theorem `AddSubgroup.closure_le` states that for any type `G` that forms an additive group, and for any additive subgroup `K` of `G` and a set `k` of elements in `G`, the closure of the set `k` with respect to the additive subgroup operation is contained within `K` if and only if the set `k` itself is contained in `K`. Here, the closure of a set `k` refers to the smallest additive subgroup that contains `k`, and `k ⊆ ↑K` represents the containment of the set `k` in the subgroup `K`. More concisely: For any additive group G, subgroup K, and set k of elements in G, the closure of k in K equals k if and only if k is contained in K.
`add_mem_cancel_right` theorem add_mem_cancel_right : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_6} {H : S} [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G] {x y : G}, x ∈ H → (y + x ∈ H ↔ y ∈ H) This theorem, `add_mem_cancel_right`, states that for any type `G` with an `AddGroup` instance, a type `S`, an element `H` of `S` with `SetLike` and `AddSubgroupClass` instances, and two elements `x` and `y` of `G`, if `x` is an element of `H`, then `y + x` is an element of `H` if and only if `y` is an element of `H`. In other words, in the context of addition groups and additive subgroups, adding an element `x` from the subgroup `H` to another element `y` results in an element that is also in `H` if and only if `y` was already in `H`. More concisely: For any additive group `G`, additive subgroup `H`, and elements `x` in `H` and `y` in `G`, if `x` is in `H` then `y + x` is in `H` if and only if `y` is in `H`.
`AddSubgroup.closure_eq` theorem AddSubgroup.closure_eq : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G), AddSubgroup.closure ↑K = K This theorem states that for any additive group `G` and any additive subgroup `K` of `G`, the additive closure of `K` is equal to `K` itself. In Lean 4, the additive closure of a set is defined as the smallest additive subgroup that contains the set. Thus, this theorem asserts that the smallest additive subgroup containing an existing additive subgroup is the subgroup itself, which intuitively makes sense as the subgroup is already closed under addition. In mathematical terms, if `G` is an additive group and `K` is a subgroup of `G`, then the closure of `K` in `G` is `K`. More concisely: The additive closure of an additive subgroup of an additive group is equal to the subgroup itself.
`sub_mem` theorem sub_mem : ∀ {M : Type u_5} {S : Type u_6} [inst : SubNegMonoid M] [inst_1 : SetLike S M] [hSM : AddSubgroupClass S M] {H : S} {x y : M}, x ∈ H → y ∈ H → x - y ∈ H This theorem states that an additive subgroup is closed under subtraction. Specifically, for any type `M` with a `SubNegMonoid` structure (a type of monoid with negation and subtraction), a set-like structure `S` of `M`, and an `AddSubgroupClass` of `S` and `M`, if you have an element `H` of `S`, and elements `x` and `y` of `M` that belong to `H`, then the difference of `x` and `y` (`x - y`) also belongs to `H`. In simpler terms, if `x` and `y` are elements of an additive subgroup `H`, then their difference is also an element of `H`. More concisely: If `H` is an additive subgroup of a `SubNegMonoid` `M`, then for all `x, y` in `H`, `x - y` is also in `H`.
`Subgroup.comap_top` theorem Subgroup.comap_top : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N), Subgroup.comap f ⊤ = ⊤ The theorem `Subgroup.comap_top` states that for any group homomorphism `f` from a group `G` to another group `N`, the preimage of the top (i.e., the whole group `N`) along `f` is the top of `G`. In other words, the preimage of the whole group `N` under `f` is the whole group `G`. This is akin to saying that the inverse image of the entire range of a function is the entire domain. More concisely: For any group homomorphism `f` from group `G` to group `N`, `f⁻¹(N) = G`.
`AddSubgroup.nontrivial_iff_exists_ne_zero` theorem AddSubgroup.nontrivial_iff_exists_ne_zero : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), Nontrivial ↥H ↔ ∃ x ∈ H, x ≠ 0 This theorem states that for any given type `G` that has an additive group structure, and any additive subgroup `H` of `G`, `H` is nontrivial if and only if there exists an element `x` in `H` such that `x` is not the zero element of the group. Nontrivial in this context means that the subgroup `H` is not just the singleton set containing the zero element of the group. More concisely: A subgroup of an additive group is nontrivial if and only if it contains a non-zero element.
`Subgroup.gc_map_comap` theorem Subgroup.gc_map_comap : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N), GaloisConnection (Subgroup.map f) (Subgroup.comap f) The theorem `Subgroup.gc_map_comap` states that for any two types `G` and `N` with `Group` instances, and any monoid homomorphism `f` from `G` to `N`, there exists a Galois connection between the function `Subgroup.map f` and `Subgroup.comap f`. In the context of groups and subgroups, this means that the image of a subgroup under the monoid homomorphism `f` is less than or equal to a subgroup in `N` if and only if the original subgroup is less than or equal to the preimage of that subgroup in `N` under `f`. This characterizes a certain correspondence between the structure of subgroups in `G` and `N` induced by the monoid homomorphism `f`. More concisely: For any group homomorphism `f` between groups `G` and `N`, there exists a Galois connection between `Subgroup.map f` and `Subgroup.comap f`, meaning that `Subgroup.map f(H) ≤ Subgroup.comap f(K)` in `N` if and only if `H ≤ K` in `G`.
`MonoidHom.eqOn_closure` theorem MonoidHom.eqOn_closure : ∀ {G : Type u_1} [inst : Group G] {M : Type u_7} [inst_1 : Monoid M] {f g : G →* M} {s : Set G}, Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(Subgroup.closure s) This theorem states that if two monoid homomorphisms, represented by functions `f` and `g`, are equal on a set `s` of elements of a group `G`, then they are also equal on the subgroup closure of that set. Here, "equal on a set" means that for every element in the set, both homomorphisms produce the same result. A subgroup closure of a set `s` in a group `G` is the smallest subgroup of `G` that contains all elements of `s`. The theorem, therefore, guarantees the consistency of two homomorphisms on the set and its subgroup closure. More concisely: If two monoid homomorphisms agree on a set, they agree on its subgroup closure.
`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.43` theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.43 : ∀ {b a : Prop}, (∃ (_ : a), b) = (a ∧ b) This theorem is in the realm of logic and propositional calculus. It states that for any two propositions 'a' and 'b', the existence of 'b' given 'a' (denoted as `∃ (_ : a), b`) is logically equivalent to the conjunction of 'a' and 'b' (denoted as `a ∧ b`). In other words, affirming that 'b' is true if 'a' is true is the same as asserting that both 'a' and 'b' are true. More concisely: The theorem asserts that for any propositions 'a' and 'b' in logic, `∃ (x : a), b` is logically equivalent to `a ∧ b`.
`MonoidHom.range_eq_map` theorem MonoidHom.range_eq_map : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N), f.range = Subgroup.map f ⊤ := by sorry The theorem `MonoidHom.range_eq_map` states that for any group homomorphism `f` from a group `G` to another group `N`, the range of `f` is equal to the image of the whole group `G` under `f`. In other words, mapping the whole group `G` to `N` using `f` covers the same set of elements in `N` as the range of `f`. More concisely: The range of a group homomorphism equals the image of the entire group under the homomorphism.
`div_mem` theorem div_mem : ∀ {M : Type u_5} {S : Type u_6} [inst : DivInvMonoid M] [inst_1 : SetLike S M] [hSM : SubgroupClass S M] {H : S} {x y : M}, x ∈ H → y ∈ H → x / y ∈ H This theorem states that a subgroup is closed under division. Specifically, for any type `M` equipped with a division and inverse operation (a `DivInvMonoid`), any set-like structure `S` over `M`, and any `SubgroupClass` `hSM` for `S` and `M`, if `x` and `y` are elements of a subgroup `H` of `S`, then the result of dividing `x` by `y` is also an element of the subgroup `H`. More concisely: If `M` is a type with division and inverse operations, `S` is a set-like structure over `M`, `hSM` is a subgroup class for `S` and `M`, and `H` is a subgroup of `S`, then for all `x, y in H`, `x / y is an element of H`.
`Subgroup.coe_eq_univ` theorem Subgroup.coe_eq_univ : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, ↑H = Set.univ ↔ H = ⊤ The theorem `Subgroup.coe_eq_univ` states that for any type `G` with a `Group` instance and any subgroup `H` of `G`, the coercion of `H` to a set is equal to the universal set of `G` if and only if `H` is the top subgroup. In mathematical terms, this means that every element of the group `G` is in the subgroup `H` if and only if `H` is the whole group `G`, which is represented by the top element (`⊤`) in the lattice of subgroups of `G`. More concisely: The coercion of the top subgroup of a group to a set equals the universal set if and only if.
`zsmul_mem` theorem zsmul_mem : ∀ {M : Type u_5} {S : Type u_6} [inst : SubNegMonoid M] [inst_1 : SetLike S M] [hSM : AddSubgroupClass S M] {K : S} {x : M}, x ∈ K → ∀ (n : ℤ), n • x ∈ K This theorem, `zsmul_mem`, states that for any type `M` which is a sub-negative monoid, any type `S` which is a set-like structure over `M`, and any `S` that is also an additive subgroup of `M`, if we have an element `x` from an instance `K` of `S`, then the integer-multiple (denoted by `n • x`) of `x` is also an element of `K`. In mathematical terms, if `x` is in a subgroup `K`, then for any integer `n`, `n` times `x` is also in the subgroup `K`. More concisely: If `x` is an element of a subgroup `K` of a sub-negative monoid `M`, then for any integer `n`, `n` times `x` is also an element of `K`.
`Subgroup.comap_map_eq_self` theorem Subgroup.comap_map_eq_self : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {H : Subgroup G}, f.ker ≤ H → Subgroup.comap f (Subgroup.map f H) = H This theorem states that for any group `G` and `N`, and a monoid homomorphism `f` from `G` to `N`, if the multiplicative kernel of `f` is a subgroup of `H` (i.e., `MonoidHom.ker f ≤ H`), then the preimage of the image of `H` under `f` (i.e., `Subgroup.comap f (Subgroup.map f H)`) is equal to `H`. In other words, if all elements `x` in `G` that map to `1` in `N` under `f` are in `H`, then applying `f` to `H` and taking the preimage gives us back `H`. More concisely: If `f` is a monoid homomorphism from group `G` to monoid `N`, `H` is a subgroup of `G`, and the multiplicative kernel of `f` is contained in `H`, then the preimage of the image of `H` under `f` is equal to `H`.
`Subgroup.map_sup` theorem Subgroup.map_sup : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H K : Subgroup G) (f : G →* N), Subgroup.map f (H ⊔ K) = Subgroup.map f H ⊔ Subgroup.map f K The theorem `Subgroup.map_sup` states that for any two subgroups `H` and `K` of a group `G`, and any group homomorphism `f` from `G` to another group `N`, the image of the join (supremum) of `H` and `K` under `f` is equal to the join (supremum) of the images of `H` and `K` under `f`. In other words, the map of the union of two subgroups is the union of the maps of the subgroups, preserving the structure of subgroups under the homomorphism. More concisely: For any group homomorphism $f : G \rightarrow N$ and subgroups $H, K \subseteq G$, $f(\sup H \cup K) = \sup f(H) \cup f(K)$.
`AddSubgroup.comap_mono` theorem AddSubgroup.comap_mono : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {K K' : AddSubgroup N}, K ≤ K' → AddSubgroup.comap f K ≤ AddSubgroup.comap f K' The theorem `AddSubgroup.comap_mono` states that for any given additively written groups `G` and `N`, and a homomorphism `f` from `G` to `N`, if we have an additive subgroup `K` of `N` that is a subset of another additive subgroup `K'` of `N` (i.e., `K ≤ K'`), then the preimage of `K` under `f` is a subset of the preimage of `K'` under `f`. In other words, the mapping of subgroups from `N` back to `G` preserves the subset relationship. More concisely: If `f` is a homomorphism from the additively written groups `G` to `N`, and `K` is a subgroup of `K'` in `N`, then `f⁻¹(K) ≤ f⁻¹(K')`.
`AddSubgroup.add_mem` theorem AddSubgroup.add_mem : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) {x y : G}, x ∈ H → y ∈ H → x + y ∈ H This theorem states that an additive subgroup is closed under the operation of addition. More specifically, if 'G' is an additive group and 'H' is an additive subgroup of 'G', then for any elements 'x' and 'y' in 'H', their sum 'x + y' also belongs to 'H'. In the language of set theory, this means that the set 'H' is closed with respect to the operation of addition. More concisely: If 'H' is an additive subgroup of an additive group 'G', then for all 'x, y ∈ H', x + y ∈ H.
`MonoidHom.rangeRestrict_surjective` theorem MonoidHom.rangeRestrict_surjective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N), Function.Surjective ⇑f.rangeRestrict The theorem `MonoidHom.rangeRestrict_surjective` states that for all groups `G` and `N` and for any group homomorphism `f` from `G` to `N`, the canonical surjective group homomorphism `MonoidHom.rangeRestrict f` is surjective. In other words, for every element in the codomain of `MonoidHom.rangeRestrict f`, there exists at least one element in the domain `G` such that the function `MonoidHom.rangeRestrict f` applied to this element gives the element in the codomain. This makes the range restriction of a group homomorphism a surjective function. More concisely: For any group homomorphism from a group to another, the range restriction is a surjective function.
`Subgroup.le_comap_map` theorem Subgroup.le_comap_map : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) (H : Subgroup G), H ≤ Subgroup.comap f (Subgroup.map f H) The theorem `Subgroup.le_comap_map` states that for any group homomorphism `f` from a group `G` to a group `N` and for any subgroup `H` of `G`, the subgroup `H` is a subset (or is less than or equal to) the preimage under `f` of the image of `H` under `f`. In other words, if we first map the subgroup `H` under the homomorphism `f` and then take the preimage of this set again under `f`, we end up with a set that is at least as large as `H`. More concisely: For any group homomorphism `f` and subgroup `H` of a group `G`, `f''(H)` (the image of `H` under `f` and then the preimage of that set under `f` again) is a subgroup of `H`. (Or, more succinctly, `f''(H) ≤ H`.)
`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.46` theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.46 : ∀ {G : Type u_1} [inst : Group G] {p p' : Subgroup G} {x : G}, (x ∈ p ⊓ p') = (x ∈ p ∧ x ∈ p') This theorem states that for any group `G`, given two subgroups `p` and `p'` of `G` and an element `x` from `G`, `x` belongs to the intersection of `p` and `p'` if and only if `x` belongs to both `p` and `p'`. This theorem is a fundamental property of the intersection operation in group theory. More concisely: For any groups G and subgroups p and p', x ∈ p ∩ p' if and only if x ∈ p and x ∈ p'.
`Subgroup.normalCore_le` theorem Subgroup.normalCore_le : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.normalCore ≤ H This theorem states that for any group `G` and any subgroup `H` of `G`, the normal core of `H` is a subgroup of `H`. In other words, every element of the normal core of `H` is also an element of `H`. The normal core of a subgroup `H` is defined as the largest normal subgroup of `G` that is contained in `H`. Here, a normal subgroup is a subgroup where each element `a` satisfies the property that for any element `b` from the group, the element resulting from the operation `b * a * b⁻¹` (where `` denotes group multiplication and `b⁻¹` denotes the inverse of `b`) is also in `H`. More concisely: The normal core of a subgroup is a subgroup containing only its normal elements.*
`Subgroup.normalizer_eq_top` theorem Subgroup.normalizer_eq_top : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.normalizer = ⊤ ↔ H.Normal This theorem states that, for any type `G` with a group structure and any subgroup `H` of `G`, the normalizer of `H` equals the top element (indicating the whole group `G`) if and only if `H` is a normal subgroup of `G`. In mathematical terms, $H$ is normal in $G$ if and only if every element of $G$ commutes with $H$ (i.e., for all $g$ in $G$ and $n$ in $H$, $g * n * g^{-1}$ is in $H$). More concisely: A subgroup `H` of a group `G` is normal if and only if the normalizer of `H` equals `G`. That is, `norm_group G H = G` if and only if `H` is a normal subgroup of `G`.
`AddSubgroup.eq_bot_of_subsingleton` theorem AddSubgroup.eq_bot_of_subsingleton : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [inst_1 : Subsingleton ↥H], H = ⊥ This theorem states that for any additive group 'G' and an additive subgroup 'H' of 'G', if 'H' is a subsingleton (meaning it contains at most one element), then 'H' is equal to the trivial group (denoted by ⊥, the bottom element). In other words, an additive subgroup of a group is trivial if and only if it is a subsingleton. More concisely: An additive subgroup of a group is the trivial subgroup if and only if it contains at most one element.
`AddSubgroup.map_normalizer_eq_of_bijective` theorem AddSubgroup.map_normalizer_eq_of_bijective : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H : AddSubgroup G) {f : G →+ N}, Function.Bijective ⇑f → AddSubgroup.map f H.normalizer = (AddSubgroup.map f H).normalizer This theorem states that for any two types `G` and `N` with `AddGroup` structures, any subgroup `H` of `G`, and any bijective function `f` mapping `G` to `N`, the image of the normalizer of `H` under the function `f` is equal to the normalizer of the image of `H` under the same function `f`. Here, a function `f` is bijective if it is both injective (each element of `N` has exactly one corresponding element in `G`) and surjective (every element of `N` corresponds to some element of `G`). The normalizer of a subgroup is the set of elements that normalize the subgroup. In the context of additive groups, the mapping of a subgroup through `f` results in another subgroup, and this theorem relates the normalizers of these subgroups when `f` is bijective. More concisely: For any bijective function `f` between additive groups `G` and `N`, the normalizer of the image of a subgroup `H` of `G` under `f` is equal to the image of the normalizer of `H` under `f`.
`AddSubgroup.closure_induction₂` theorem AddSubgroup.closure_induction₂ : ∀ {G : Type u_1} [inst : AddGroup G] {k : Set G} {p : G → G → Prop} {x y : G}, x ∈ AddSubgroup.closure k → y ∈ AddSubgroup.closure k → (∀ x ∈ k, ∀ y ∈ k, p x y) → (∀ (x : G), p 0 x) → (∀ (x : G), p x 0) → (∀ (x₁ x₂ y : G), p x₁ y → p x₂ y → p (x₁ + x₂) y) → (∀ (x y₁ y₂ : G), p x y₁ → p x y₂ → p x (y₁ + y₂)) → (∀ (x y : G), p x y → p (-x) y) → (∀ (x y : G), p x y → p x (-y)) → p x y This theorem provides an induction principle for proving properties about pairs of elements in the additive closure of a set in an additive group. If we have a function `p` from pairs of group elements to propositions, and `x` and `y` are two elements in the additive closure of a set `k` in the group, then `p x y` holds if the following conditions are met: 1. `p` holds for every pair of elements in `k`. 2. `p` holds for zero and any element in the group. 3. `p` holds for any element in the group and zero. 4. If `p` holds for `x₁` and `y`, and `p` holds for `x₂` and `y`, then `p` also holds for the sum of `x₁` and `x₂` and `y`. 5. If `p` holds for `x` and `y₁`, and `p` holds for `x` and `y₂`, then `p` also holds for `x` and the sum of `y₁` and `y₂`. 6. If `p` holds for `x` and `y`, then `p` also holds for the negation of `x` and `y`. 7. If `p` holds for `x` and `y`, then `p` also holds for `x` and the negation of `y`. More concisely: The theorem asserts that if a property `p` holds for all pairs of elements in a set `k` in an additive group, and satisfies certain conditions with respect to addition and zero, then `p` holds for any pair of elements in the additive closure of `k`.
`Subgroup.IsCommutative.is_comm` theorem Subgroup.IsCommutative.is_comm : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.IsCommutative → Std.Commutative fun x x_1 => x * x_1 := by sorry The theorem states that for any given group `G` and any subgroup `H` of `G`, if `H` has the property of being commutative, then the multiplication operation (``) on elements of `H` is also commutative. In other words, for every pair of elements `x` and `x_1` in subgroup `H`, the result of `x x_1` is the same as `x_1 * x`. Here, `Std.Commutative` is a predicate that checks if an operation (in this case, multiplication) is commutative. More concisely: If `H` is a commutative subgroup of the group `G`, then the multiplication of any two elements in `H` is commutative.
`Subgroup.map_injective_of_ker_le` theorem Subgroup.map_injective_of_ker_le : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) {H K : Subgroup G}, f.ker ≤ H → f.ker ≤ K → Subgroup.map f H = Subgroup.map f K → H = K The theorem `Subgroup.map_injective_of_ker_le` states that given two subgroups `H` and `K` of a group `G` and a group homomorphism `f` from `G` to another group `N`, if the kernel of `f` is a subset of both `H` and `K` and the image of `H` and `K` under `f` are equal, then `H` and `K` must be the same subgroup. In other words, if two subgroups of a group map to the same subgroup in the target group under a group homomorphism, and both subgroups contain all the elements that map to the identity in the target group, then the two subgroups are identical. More concisely: If two subgroups of a group have the same image under a group homomorphism and contain all of its kernel, then they are equal.
`AddSubgroup.mem_sup` theorem AddSubgroup.mem_sup : ∀ {C : Type u_6} [inst : AddCommGroup C] {s t : AddSubgroup C} {x : C}, x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y + z = x This theorem states that for any type `C` which forms an additive commutative group, and for any two additive subgroups `s` and `t` of this group, an element `x` belongs to the supremum (join) of `s` and `t` if and only if there exist elements `y` in `s` and `z` in `t` such that their sum `y + z` equals `x`. More concisely: For any additive commutative group `C` and subgroups `s` and `t`, an element `x` is in the supremum of `s` and `t` if and only if there exist `y` in `s` and `z` in `t` such that `x = y + z`.
`Subgroup.subset_normalClosure` theorem Subgroup.subset_normalClosure : ∀ {G : Type u_1} [inst : Group G] {s : Set G}, s ⊆ ↑(Subgroup.normalClosure s) This theorem states that for any group `G` and any set `s` of elements from `G`, `s` is a subset of the normal closure of `s`. In other words, all elements of `s` are included in the smallest normal subgroup that contains all the conjugates of elements of `s`. This is a fundamental characteristic of the normal closure in group theory. More concisely: The normal closure of a set of elements in a group is the smallest normal subgroup containing all conjugates of those elements.
`zpow_mem` theorem zpow_mem : ∀ {M : Type u_5} {S : Type u_6} [inst : DivInvMonoid M] [inst_1 : SetLike S M] [hSM : SubgroupClass S M] {K : S} {x : M}, x ∈ K → ∀ (n : ℤ), x ^ n ∈ K This theorem states that for any type `M` with a division and inversion operation structure (`DivInvMonoid`) and any type `S` that behaves like a set of `M` and forms a subgroup (`SubgroupClass`), given a subgroup `K` of type `S` and an element `x` in `M` that belongs to `K`, then the integer power (`n : ℤ`) of `x` (denoted by `x ^ n`) also belongs to `K`. This theorem essentially means that the power of any element in a subgroup remains in the subgroup, which is a fundamental property of mathematical groups. More concisely: If `M` is a `DivInvMonoid` type with subgroup `S` (as a `SubgroupClass`), then for any `x` in `M` in `S` and `n` in `ℤ`, `x ^ n` is also in `S`.
`Subgroup.characteristic_iff_comap_eq` theorem Subgroup.characteristic_iff_comap_eq : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.Characteristic ↔ ∀ (ϕ : G ≃* G), Subgroup.comap ϕ.toMonoidHom H = H This theorem states that for any group `G` and any subgroup `H` of `G`, `H` is characteristic if and only if, for every multiplicative equivalence `ϕ` from `G` to itself, the preimage of `H` under the monoid homomorphism associated with `ϕ` is equal to `H`. In other words, a subgroup `H` of a group `G` is characteristic if and only if it remains unchanged under any automorphism of `G`. More concisely: A subgroup of a group is characteristic if and only if it is mapped to itself under every automorphism of the group.
`AddSubgroup.addCommute_of_normal_of_disjoint` theorem AddSubgroup.addCommute_of_normal_of_disjoint : ∀ {G : Type u_1} [inst : AddGroup G] (H₁ H₂ : AddSubgroup G), H₁.Normal → H₂.Normal → Disjoint H₁ H₂ → ∀ (x y : G), x ∈ H₁ → y ∈ H₂ → AddCommute x y The theorem `AddSubgroup.addCommute_of_normal_of_disjoint` states that for any type `G` that has an addition group structure, if `H₁` and `H₂` are normal subgroups of `G` and they are disjoint (meaning that their greatest lower bound is the bottom element of the lattice), then for any elements `x` and `y` such that `x` belongs to `H₁` and `y` belongs to `H₂`, these elements commute under addition, i.e., `x + y = y + x`. In other words, the elements of disjoint, normal subgroups of an additive group are commutative. More concisely: If `G` is an additive group, `H₁` and `H₂` are normal, disjoint subgroups of `G`, then for all `x ∈ H₁` and `y ∈ H₂`, `x + y = y + x`.
`AddSubgroup.characteristic_iff_comap_eq` theorem AddSubgroup.characteristic_iff_comap_eq : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.Characteristic ↔ ∀ (ϕ : G ≃+ G), AddSubgroup.comap ϕ.toAddMonoidHom H = H The theorem `AddSubgroup.characteristic_iff_comap_eq` states that for any additive group `G` and any additive subgroup `H` of `G`, `H` is a characteristic subgroup if and only if for every additive equivalence (a bijective, addition-preserving function) `ϕ` from `G` to `G`, the preimage of `H` under the corresponding additive monoid homomorphism of `ϕ` is equal to `H` itself. In other words, a characteristic subgroup is one that is invariant under all automorphisms (self-isomorphisms) of the additive group. More concisely: A subgroup H of an additive group G is characteristic if and only if for all additive equivalences φ from G to G, φ⁻¹(H) = H.
`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.107` theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.107 : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N}, Function.Injective ⇑f.rangeRestrict = Function.Injective ⇑f The theorem states that for any groups `G` and `N`, and a monoid homomorphism `f` from `G` to `N`, a member `y` of `N` belongs to the range of `f` if and only if there exists an element `x` in `G` such that `f(x) = y`. This essentially asserts the definition of the range of a function in the context of group theory and monoid homomorphisms. More concisely: For any group homomorphism f from group G to monoid N, the image of an element y in N under f is precisely some x in G.
`AddSubgroup.map_injective_of_ker_le` theorem AddSubgroup.map_injective_of_ker_le : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) {H K : AddSubgroup G}, f.ker ≤ H → f.ker ≤ K → AddSubgroup.map f H = AddSubgroup.map f K → H = K This theorem states that for any given additive group homomorphism `f` from a group `G` to a group `N`, and any two subgroups `H` and `K` of `G`, if the kernel of `f` is a subset of both `H` and `K`, and the images of `H` and `K` under the homomorphism `f` are equal, then `H` and `K` must be the same subgroup. In more mathematical terms, given `f : G → N` is a group homomorphism, `H` and `K` are subgroups of `G`, and conditions `f.ker ≤ H`, `f.ker ≤ K`, and `f(H) = f(K)`, it follows that `H = K`. More concisely: If `f : G → N` is a group homomorphism, `H` and `K` are subgroups of `G`, and `f.ker ≤ H`, `f.ker ≤ K`, and `f(H) = f(K)`, then `H = K`.
`AddMonoidHom.range_eq_map` theorem AddMonoidHom.range_eq_map : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N), f.range = AddSubgroup.map f ⊤ This theorem states that for any addition group homomorphism `f` from an additive group `G` to another additive group `N`, the range of `f` is equal to the image of the entire group `G` (denoted as `⊤` for the top element in lattice theory, representing the whole set in this context) under the map `f`. Essentially, this expresses the fact that the range of a group homomorphism is the same as the set of all elements in the codomain that are hit by the map when applied to every element in the domain. More concisely: For any additive group homomorphism from group G to group N, the range of the homomorphism is equal to the image of G under the map.
`AddSubgroup.coe_add` theorem AddSubgroup.coe_add : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (x y : ↥H), ↑(x + y) = ↑x + ↑y This theorem states that for any additive group `G` and any additive subgroup `H` of `G`, the sum of two elements `x` and `y` in the subgroup `H` is the same whether the sum is computed inside the subgroup or in the containing group. In other words, the act of summing two elements is the same regardless if it's done in the larger group `G` or the subgroup `H`; the coercion of the sum from the subgroup to the group is the same as the sum of the individual coercions. More concisely: For any additive group G and additive subgroup H, the sum of two elements in H is equal to their sum in G.
`Subgroup.eq_bot_of_subsingleton` theorem Subgroup.eq_bot_of_subsingleton : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst_1 : Subsingleton ↥H], H = ⊥ This theorem states that for any type `G` which has a group structure, if `H` is a subgroup of `G` and this subgroup `H` is a subsingleton (that is, it contains at most one element), then `H` must be the trivial group (denoted as `⊥`). In other words, any subsingleton subgroup of a group is the trivial group. More concisely: For any group `G`, if `H` is a subgroup of `G` with at most one element, then `H` is the trivial group `⊥`.
`Subgroup.closure_induction₂` theorem Subgroup.closure_induction₂ : ∀ {G : Type u_1} [inst : Group G] {k : Set G} {p : G → G → Prop} {x y : G}, x ∈ Subgroup.closure k → y ∈ Subgroup.closure k → (∀ x ∈ k, ∀ y ∈ k, p x y) → (∀ (x : G), p 1 x) → (∀ (x : G), p x 1) → (∀ (x₁ x₂ y : G), p x₁ y → p x₂ y → p (x₁ * x₂) y) → (∀ (x y₁ y₂ : G), p x y₁ → p x y₂ → p x (y₁ * y₂)) → (∀ (x y : G), p x y → p x⁻¹ y) → (∀ (x y : G), p x y → p x y⁻¹) → p x y This theorem is an induction principle for closure membership for predicates with two arguments in the context of groups. Given a group `G`, a set `k` within `G`, and a predicate `p` that operates on two elements of `G`, if both `x` and `y` are elements of the subgroup generated by `k`, and assuming a number of properties of `p` (namely, its behavior regarding the group identity, its behavior under multiplication of the first or the second argument, and its behavior under taking inverses of both arguments), then `p x y` holds. In other words, this theorem shows that if a binary predicate holds for all pairs of elements in a generating set of a subgroup, and also meets certain algebraic properties, then it holds for all pairs of elements in the whole subgroup. This is a generalized principle of mathematical induction in the context of group theory. More concisely: Given a group `G`, a set `k` generating a subgroup, and a binary predicate `p` satisfying certain algebraic properties, if `p x y` holds for all `x, y ∈ k`, then `p x y` holds for all `x, y ∈ subgroup generated by k`.
`Subgroup.map_normalizer_eq_of_bijective` theorem Subgroup.map_normalizer_eq_of_bijective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H : Subgroup G) {f : G →* N}, Function.Bijective ⇑f → Subgroup.map f H.normalizer = (Subgroup.map f H).normalizer The theorem `Subgroup.map_normalizer_eq_of_bijective` states that, in the context of two groups G and N, for any subgroup H of group G and for any bijective monoid homomorphism 'f' from G to N, the image of the normalizer of H under 'f' is equal to the normalizer of the image of H under 'f'. In simpler words, if we have a way to translate between two groups that is a one-to-one correspondence (bijective), then the subgroup that normalizes another subgroup in the original group translates to the subgroup that normalizes the translated subgroup in the target group. More concisely: For any bijective group homomorphism f between groups G and N, normalizer(H)^f = normalizer(f(H)) for any subgroup H of G.

LeanAide GPT-4 documentation

Module: Mathlib.GroupTheory.Subgroup.Basic

Subgroup.comap_mono

theorem Subgroup.comap_mono : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {K K' : Subgroup N}, K ≤ K' → Subgroup.comap f K ≤ Subgroup.comap f K'

AddSubgroup.map_sup

theorem AddSubgroup.map_sup : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H K : AddSubgroup G) (f : G →+ N), AddSubgroup.map f (H ⊔ K) = AddSubgroup.map f H ⊔ AddSubgroup.map f K

AddSubgroup.le_comap_map

theorem AddSubgroup.le_comap_map : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (H : AddSubgroup G), H ≤ AddSubgroup.comap f (AddSubgroup.map f H)

Subgroup.subtype_injective

theorem Subgroup.subtype_injective : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), Function.Injective ⇑H.subtype

Subgroup.pow_mem

theorem Subgroup.pow_mem : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) {x : G}, x ∈ K → ∀ (n : ℕ), x ^ n ∈ K

Mathlib.GroupTheory.Subgroup.Basic._auxLemma.2

theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.2 : ∀ {S : Type u_5} {G : Type u_6} [inst : InvolutiveNeg G] {x : SetLike S G} [inst_1 : NegMemClass S G] {H : S} {x_1 : G}, (-x_1 ∈ H) = (x_1 ∈ H)

Mathlib.GroupTheory.Subgroup.Basic._auxLemma.39

theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.39 : ∀ {G : Type u_1} [inst : AddGroup G] (x : G), (x ∈ ⊤) = True

Subgroup.inv_mem_iff

theorem Subgroup.inv_mem_iff : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) {x : G}, x⁻¹ ∈ H ↔ x ∈ H

AddSubgroup.coe_eq_univ

theorem AddSubgroup.coe_eq_univ : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, ↑H = Set.univ ↔ H = ⊤ := by sorry

Mathlib.GroupTheory.Subgroup.Basic._auxLemma.38

theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.38 : ∀ {G : Type u_1} [inst : Group G] (x : G), (x ∈ ⊤) = True

Subgroup.coe_mk

theorem Subgroup.coe_mk : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (x : G) (hx : x ∈ H), ↑⟨x, hx⟩ = x := by sorry

Mathlib.GroupTheory.Subgroup.Basic._auxLemma.19

theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.19 : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) (x : G), (x ∈ K.toAddSubmonoid) = (x ∈ K)

Subgroup.closure_le

theorem Subgroup.closure_le : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) {k : Set G}, Subgroup.closure k ≤ K ↔ k ⊆ ↑K

AddSubgroup.gc_map_comap

theorem AddSubgroup.gc_map_comap : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N), GaloisConnection (AddSubgroup.map f) (AddSubgroup.comap f)

MonoidHom.map_range

theorem MonoidHom.map_range : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} {P : Type u_6} [inst_1 : Group N] [inst_2 : Group P] (g : N →* P) (f : G →* N), Subgroup.map g f.range = (g.comp f).range

Subgroup.map_top_of_surjective

theorem Subgroup.map_top_of_surjective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N), Function.Surjective ⇑f → Subgroup.map f ⊤ = ⊤

Mathlib.GroupTheory.Subgroup.Basic._auxLemma.76

theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.76 : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} {h : ↥K}, (h ∈ H.subgroupOf K) = (↑h ∈ H)

Subgroup.closure_eq

theorem Subgroup.closure_eq : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G), Subgroup.closure ↑K = K

AddSubgroup.IsCommutative.is_comm

theorem AddSubgroup.IsCommutative.is_comm : ∀ {A : Type u_4} [inst : AddGroup A] {H : AddSubgroup A}, H.IsCommutative → Std.Commutative fun x x_1 => x + x_1

Subgroup.Characteristic.fixed

theorem Subgroup.Characteristic.fixed : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.Characteristic → ∀ (ϕ : G ≃* G), Subgroup.comap ϕ.toMonoidHom H = H

AddSubgroup.closure_union

theorem AddSubgroup.closure_union : ∀ {G : Type u_1} [inst : AddGroup G] (s t : Set G), AddSubgroup.closure (s ∪ t) = AddSubgroup.closure s ⊔ AddSubgroup.closure t

Mathlib.GroupTheory.Subgroup.Basic._auxLemma.37

theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.37 : ∀ {G : Type u_1} [inst : AddGroup G] {x : G}, (x ∈ ⊥) = (x = 0)

AddSubgroup.Characteristic.fixed

theorem AddSubgroup.Characteristic.fixed : ∀ {A : Type u_4} [inst : AddGroup A] {H : AddSubgroup A}, H.Characteristic → ∀ (ϕ : A ≃+ A), AddSubgroup.comap ϕ.toAddMonoidHom H = H

AddSubgroup.map_mono

theorem AddSubgroup.map_mono : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {K K' : AddSubgroup G}, K ≤ K' → AddSubgroup.map f K ≤ AddSubgroup.map f K'

NegMemClass.neg_mem

theorem NegMemClass.neg_mem : ∀ {S : Type u_5} {G : Type u_6} [inst : Neg G] [inst_1 : SetLike S G] [self : NegMemClass S G] {s : S} {x : G}, x ∈ s → -x ∈ s

Mathlib.GroupTheory.Subgroup.Basic._auxLemma.89

theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.89 : ∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → Group (f i)] (I : Set η) {H : (i : η) → Subgroup (f i)} {p : (i : η) → f i}, (p ∈ Subgroup.pi I H) = ∀ i ∈ I, p i ∈ H i

AddSubgroup.subtype_range

theorem AddSubgroup.subtype_range : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.subtype.range = H := by sorry

neg_mem_iff

theorem neg_mem_iff : ∀ {S : Type u_5} {G : Type u_6} [inst : InvolutiveNeg G] {x : SetLike S G} [inst_1 : NegMemClass S G] {H : S} {x_1 : G}, -x_1 ∈ H ↔ x_1 ∈ H

Mathlib.GroupTheory.Subgroup.Basic._auxLemma.108

theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.108 : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N}, Function.Injective ⇑f.rangeRestrict = Function.Injective ⇑f

Subgroup.mem_bot

theorem Subgroup.mem_bot : ∀ {G : Type u_1} [inst : Group G] {x : G}, x ∈ ⊥ ↔ x = 1

AddSubgroup.coeSubtype

theorem AddSubgroup.coeSubtype : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), ⇑H.subtype = Subtype.val

AddSubgroup.coe_map

theorem AddSubgroup.coe_map : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (K : AddSubgroup G), ↑(AddSubgroup.map f K) = ⇑f '' ↑K

Subgroup.div_mem

theorem Subgroup.div_mem : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) {x y : G}, x ∈ H → y ∈ H → x / y ∈ H := by sorry

Subgroup.comap_normalizer_eq_of_surjective

theorem Subgroup.comap_normalizer_eq_of_surjective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H : Subgroup G) {f : N →* G}, Function.Surjective ⇑f → Subgroup.comap f H.normalizer = (Subgroup.comap f H).normalizer

Subgroup.one_mem

theorem Subgroup.one_mem : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), 1 ∈ H

Mathlib.GroupTheory.Subgroup.Basic._auxAddLemma.76

theorem Mathlib.GroupTheory.Subgroup.Basic._auxAddLemma.76 : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} {h : ↥K}, (h ∈ H.addSubgroupOf K) = (↑h ∈ H)

AddSubgroup.mem_closure_singleton

theorem AddSubgroup.mem_closure_singleton : ∀ {G : Type u_1} [inst : AddGroup G] {x y : G}, y ∈ AddSubgroup.closure {x} ↔ ∃ n, n • x = y

Mathlib.GroupTheory.Subgroup.Basic._auxLemma.69

theorem Mathlib.GroupTheory.Subgroup.Basic._auxLemma.69 : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {K : Subgroup N} {f : G →* N} {x : G}, (x ∈ Subgroup.comap f K) = (f x ∈ K)

Subgroup.ker_le_comap

theorem Subgroup.ker_le_comap : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) (H : Subgroup N), f.ker ≤ Subgroup.comap f H

`Subgroup.comap_mono`

`AddSubgroup.map_sup`

`AddSubgroup.le_comap_map`

`Subgroup.subtype_injective`

`Subgroup.pow_mem`

`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.2`

`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.39`

`Subgroup.inv_mem_iff`

`AddSubgroup.coe_eq_univ`

`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.38`

`Subgroup.coe_mk`

`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.19`

`Subgroup.closure_le`

`AddSubgroup.gc_map_comap`

`MonoidHom.map_range`

`Subgroup.map_top_of_surjective`

`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.76`

`Subgroup.closure_eq`

`AddSubgroup.IsCommutative.is_comm`

`Subgroup.Characteristic.fixed`

`AddSubgroup.closure_union`

`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.37`

`AddSubgroup.Characteristic.fixed`

`AddSubgroup.map_mono`

`NegMemClass.neg_mem`

`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.89`

`AddSubgroup.subtype_range`

`neg_mem_iff`

`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.108`

`Subgroup.mem_bot`

`AddSubgroup.coeSubtype`

`AddSubgroup.coe_map`

`Subgroup.div_mem`

`Subgroup.comap_normalizer_eq_of_surjective`

`Subgroup.one_mem`

`Mathlib.GroupTheory.Subgroup.Basic._auxAddLemma.76`

`AddSubgroup.mem_closure_singleton`

`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.69`

`Subgroup.ker_le_comap`

`AddSubgroup.mem_top`

`Subgroup.ext`

`AddSubgroup.zero_mem`

`AddSubgroup.map_le_iff_le_comap`

`AddMonoidHom.map_range`

`Subgroup.inclusion_injective`

`Subgroup.nontrivial_iff_exists_ne_one`

`AddSubgroup.normal_addSubgroupOf_iff`

`InvMemClass.inv_mem`

`Subgroup.map_comap_eq_self`

`Subgroup.map_equiv_normalizer_eq`

`Subgroup.normal_le_normalCore`

`AddMonoidHom.ker_eq_bot_iff`

`Subgroup.Normal.conj_mem`

`Subgroup.comap_map_eq`

`AddMonoidHom.range_top_of_surjective`

`Subgroup.inv_mem'`

`Subgroup.mem_comap`

`normalizerCondition_iff_only_full_group_self_normalizing`

`add_mem_cancel_left`

`AddSubgroup.le_normalizer_comap`

`Subgroup.le_normalizer_map`

`Subgroup.Normal.mem_comm_iff`

`AddSubgroup.Normal.comap`

`AddSubgroup.closure_induction'`

`AddSubgroup.coe_neg`

`Subgroup.bot_or_exists_ne_one`

`Mathlib.GroupTheory.Subgroup.Basic._auxLemma.71`

`Subgroup.map_equiv_eq_comap_symm'`

`AddMonoidHom.range_top_iff_surjective`

`Subgroup.normal_subgroupOf_iff`

`Subgroup.map_comap_eq`

`Subgroup.eq_top_iff'`

`Subgroup.subset_closure`

`Mathlib.GroupTheory.Subgroup.Basic._auxAddLemma.89`