Mathlib.Deprecated.Subgroup._auxLemma.2
theorem Mathlib.Deprecated.Subgroup._auxLemma.2 :
∀ {G : Type u_1} [inst : AddGroup G] {g : G}, (g ∈ IsAddSubgroup.trivial G) = (g = 0)
This theorem states that for any type `G` that has an additive group structure, an element `g` of `G` belongs to the trivial additive subgroup of `G` if and only if that element `g` is equal to the additive identity element `0`. The trivial additive subgroup is defined as the set containing only the additive identity element `0`.
More concisely: For any additive group `G`, an element `g` lies in the trivial subgroup if and only if `g = 0`.
|
IsGroupHom.mem_ker
theorem IsGroupHom.mem_ker :
∀ {G : Type u_1} {H : Type u_2} [inst : Group H] (f : G → H) {x : G}, x ∈ IsGroupHom.ker f ↔ f x = 1
This theorem states that for any types `G` and `H`, with `H` being a group, and any function `f` from `G` to `H`, an element `x` of `G` is in the kernel of `f` (i.e., maps to the identity of `H`) if and only if the function `f` applied to `x` equals the identity element of the group `H`. It provides a characterization of the kernel of a group homomorphism as the preimage of the trivial subgroup of `H` (i.e., the subgroup consisting only of the identity). In mathematical terms, for a group homomorphism `f : G → H`, `x` lies in `ker(f)` if and only if `f(x) = 1`.
More concisely: For any group homomorphism f : G -> H, an element x of G lies in the kernel of f if and only if f(x) = 1.
|
AddGroup.subset_closure
theorem AddGroup.subset_closure : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G}, s ⊆ AddGroup.closure s
The theorem `AddGroup.subset_closure` states that for any type `G` that forms an additive group, and for any set `s` of elements of `G`, the set `s` is a subset of the closure of `s` under the group operation. In other words, every element of the set `s` is included in the smallest additive subgroup generated by `s`.
More concisely: For any additive group `G` and set `s` of its elements, `s` is a subset of the subgroup generated by `s`.
|
AddGroup.closure_subset
theorem AddGroup.closure_subset :
∀ {G : Type u_1} [inst : AddGroup G] {s t : Set G}, IsAddSubgroup t → s ⊆ t → AddGroup.closure s ⊆ t
The theorem `AddGroup.closure_subset` states that for any type `G` that has an additive group structure (denoted as `AddGroup G`), and for any two sets `s` and `t` of elements of `G`, if `t` is an additive subgroup and all elements of `s` are contained within `t` (expressed as `s ⊆ t`), then the additive subgroup generated by `s` (given as `AddGroup.closure s`) is also contained within `t`. In other words, the smallest additive subgroup containing `s` is a subset of any additive subgroup that contains `s`.
More concisely: For any additive group `G` and sets `s` and `t` of its elements with `s ⊆ t` and `t` an additive subgroup, `AddGroup.closure s` is contained in `t`.
|
Group.closure.isSubgroup
theorem Group.closure.isSubgroup : ∀ {G : Type u_1} [inst : Group G] (s : Set G), IsSubgroup (Group.closure s) := by
sorry
The theorem `Group.closure.isSubgroup` states that for any type `G` that has a group structure (denoted by `[inst : Group G]`), and for any set `s` of elements of `G` (denoted by `(s : Set G)`), the closure of `s` under the group operation is itself a subgroup of `G`. In other words, if you take any set of elements from a group and generate all possible elements from them through the group operation, the resulting set is also a subgroup of the original group.
More concisely: If `G` is a group and `s` is a subset of `G`, then the closure of `s` under the group operation is a subgroup of `G`.
|
IsNormalAddSubgroup.normal
theorem IsNormalAddSubgroup.normal :
∀ {A : Type u_3} [inst : AddGroup A] {s : Set A}, IsNormalAddSubgroup s → ∀ n ∈ s, ∀ (g : A), g + n + -g ∈ s := by
sorry
The theorem `IsNormalAddSubgroup.normal` states that for any type `A` equipped with an additive group structure, and for any set `s` of elements from `A`, if `s` forms a normal additive subgroup, then for any element `n` in `s` and any other element `g` from `A`, the result of adding `g` to `n`, and then subtracting `g` (or equivalently, the additive conjugate of `n` by `g`), is also an element of `s`. In other words, the set `s` is closed under additive conjugation.
More concisely: If `s` is a normal additive subgroup of an additive group `A`, then for all `n` in `s` and `g` in `A`, `n + g` and `n - g` are also in `s`.
|
AddGroup.mem_closure
theorem AddGroup.mem_closure :
∀ {G : Type u_1} [inst : AddGroup G] {s : Set G} {a : G}, a ∈ s → a ∈ AddGroup.closure s
This theorem states that for any type `G` that is an additive group, and for any set `s` of elements of type `G`, any element `a` of `G` that belongs to the set `s` also belongs to the closure of `s` under the additive group operation. Thus, the additive group generated by `s` (denoted by `AddGroup.closure s`), which is the smallest additive group containing `s`, always includes every element of `s`.
More concisely: For any additive group `G` and set `s` of its elements, every element `a` in `s` lies in the closure of `s` under the additive group operation. Equivalently, the additive group generated by `s` includes `s`.
|
Mathlib.Deprecated.Subgroup._auxLemma.1
theorem Mathlib.Deprecated.Subgroup._auxLemma.1 :
∀ {G : Type u_1} [inst : Group G] {g : G}, (g ∈ IsSubgroup.trivial G) = (g = 1)
The theorem states that for any group `G` and any element `g` in `G`, `g` belongs to the trivial subgroup of `G` if and only if `g` is equal to the identity element of `G`. The trivial subgroup of a group is the subgroup consisting only of the identity element.
More concisely: For any group G and its identity element e, g belongs to the trivial subgroup of G if and only if g = e.
|
Group.closure_subset
theorem Group.closure_subset :
∀ {G : Type u_1} [inst : Group G] {s t : Set G}, IsSubgroup t → s ⊆ t → Group.closure s ⊆ t
The theorem `Group.closure_subset` states that for any type `G` that forms a group, and for any subsets `s` and `t` of `G`, if `t` is a subgroup of `G` and `s` is a subset of `t`, then the closure of `s` (i.e., the smallest subgroup of `G` containing `s`) is also a subset of `t`. In other words, if a set `s` is contained in a subgroup, then the smallest subgroup generated by `s` is also contained within that same subgroup.
More concisely: For any group `G`, if `s` is a subset of subgroup `t` of `G`, then the closure of `s` in `G` is contained in `t`.
|
Group.normalClosure_subset
theorem Group.normalClosure_subset :
∀ {G : Type u_1} [inst : Group G] {s t : Set G}, IsNormalSubgroup t → s ⊆ t → Group.normalClosure s ⊆ t
The theorem `Group.normalClosure_subset` states that for any group `G` and any sets `s` and `t` of elements of `G`, if `t` is a normal subgroup of `G` and `s` is a subset of `t`, then the normal closure of `s` is also a subset of `t`. In other words, the smallest normal subgroup containing a given set is always contained within any larger normal subgroup that also contains that set.
More concisely: If `s` is a subset of the normal subgroup `t` of a group `G`, then the normal closure of `s` is contained in `t`.
|
Group.subset_closure
theorem Group.subset_closure : ∀ {G : Type u_1} [inst : Group G] {s : Set G}, s ⊆ Group.closure s
The theorem `Group.subset_closure` asserts that for any given group `G` and a set `s` of elements of `G`, the set `s` is a subset of the closure of `s` in `G`. In other words, every element of `s` is contained in the subgroup generated by `s`. This is a fundamental property of the closure of a set in a group, that is, the smallest subgroup of `G` that contains the set `s`.
More concisely: For any group (G : Type*) and set (s : Set G), s is a subset of the closure of s in G, i.e., every element of s is contained in the subgroup generated by s.
|
Group.normalClosure.isSubgroup
theorem Group.normalClosure.isSubgroup :
∀ {G : Type u_1} [inst : Group G] (s : Set G), IsSubgroup (Group.normalClosure s)
This theorem states that for any set `s` in a group `G`, the normal closure of `s` is itself a subgroup of `G`. In other words, given any group `G` and any set `s` of elements from `G`, if we take the normal closure of `s` (which is the subgroup closure of all the conjugates of elements of `s`), the resulting set is a subgroup of `G`. This holds true for all groups and sets of elements from those groups.
More concisely: The normal closure of any set of elements in a group is a subgroup of the group.
|
IsAddSubgroup.neg_mem
theorem IsAddSubgroup.neg_mem :
∀ {A : Type u_3} [inst : AddGroup A] {s : Set A}, IsAddSubgroup s → ∀ {a : A}, a ∈ s → -a ∈ s
This theorem states that if we have a set `s` of some type `A`, where `A` is an additive group, and if `s` is an additive subgroup of `A`, then for every element `a` in `s`, the negation of `a` (denoted by `-a`) is also in `s`. In simpler terms, this theorem states that an additive subgroup is closed under negation, i.e., if you take any element from the subgroup and negate it, the result is still in the subgroup.
More concisely: If `s` is an additive subgroup of an additive group `A`, then for all `a` in `s`, `-a` is also in `s`.
|
IsSubgroup.inv_mem
theorem IsSubgroup.inv_mem : ∀ {G : Type u_1} [inst : Group G] {s : Set G}, IsSubgroup s → ∀ {a : G}, a ∈ s → a⁻¹ ∈ s
The theorem `IsSubgroup.inv_mem` states that for any type `G` that has a group structure, and any set `s` of elements of that type `G`, if `s` forms a subgroup, then for any element `a` in `s`, the inverse of `a` (denoted by `a⁻¹`) is also an element of `s`. In other words, the set `s` is closed under the operation of taking inverses, which is one of the properties required for `s` to be a subgroup.
More concisely: If `s` is a subgroup of the group `G`, then for all `a` in `s`, the inverse `a⁻¹` is also in `s`.
|
Group.normalClosure.is_normal
theorem Group.normalClosure.is_normal :
∀ {G : Type u_1} {s : Set G} [inst : Group G], IsNormalSubgroup (Group.normalClosure s)
This theorem states that for any set `s` in a group `G`, the normal closure of `s` is a normal subgroup. In other words, every normal closure in a group is a normal subgroup. Here, the normal closure of a set is defined as the subgroup closure of all the conjugates of elements of the set; it is the smallest normal subgroup containing the set. The theorem verifies this by showing that a normal closure satisfies the properties required of a normal subgroup.
More concisely: The normal closure of any set in a group is a normal subgroup.
|
IsAddGroupHom.image_addSubgroup
theorem IsAddGroupHom.image_addSubgroup :
∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] {f : G → H},
IsAddGroupHom f → ∀ {s : Set G}, IsAddSubgroup s → IsAddSubgroup (f '' s)
This theorem, named `IsAddGroupHom.image_addSubgroup`, asserts that for any two additive groups `G` and `H` and a function `f` from `G` to `H`, if `f` is an additive group homomorphism and `s` is an additive subgroup of `G`, then the image of `s` under `f` is an additive subgroup of `H`. In other words, the image of an additive subgroup under an additive group homomorphism is also an additive subgroup.
More concisely: Given an additive group `H`, an additive group `G`, and an additive group homomorphism `f` from `G` to `H`, the image of an additive subgroup `s` of `G` under `f` is an additive subgroup of `H`.
|
AddGroup.closure.isAddSubgroup
theorem AddGroup.closure.isAddSubgroup :
∀ {G : Type u_1} [inst : AddGroup G] (s : Set G), IsAddSubgroup (AddGroup.closure s)
The theorem `AddGroup.closure.isAddSubgroup` states that for any type `G` that forms an additive group, and for any set `s` of elements of type `G`, the closure of `s` under the operation of the additive group, denoted as `AddGroup.closure s`, forms an additive subgroup. In other words, the smallest additive subgroup that contains the set `s` is itself an additive subgroup.
More concisely: The closure of any set in an additive group under the group operation is an additive subgroup.
|
IsAddGroupHom.mem_ker
theorem IsAddGroupHom.mem_ker :
∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup H] (f : G → H) {x : G}, x ∈ IsAddGroupHom.ker f ↔ f x = 0 := by
sorry
This theorem states that for any two types `G` and `H` where `H` is an additive group, and for any function `f` from `G` to `H` and any element `x` of `G`, the element `x` belongs to the kernel of `f` if and only if the function `f` applied to `x` equals the additive identity (0) in `H`. In mathematical terms, it states that for a function `f: G → H`, an element `x` is in the kernel of `f` (the preimage of the trivial subgroup of `H`) if and only if `f(x) = 0`.
More concisely: For any additive group `H` and function `f` from a type `G` to `H`, an element `x` in `G` belongs to the kernel of `f` if and only if `f(x) = 0`.
|
IsNormalSubgroup.normal
theorem IsNormalSubgroup.normal :
∀ {G : Type u_1} [inst : Group G] {s : Set G}, IsNormalSubgroup s → ∀ n ∈ s, ∀ (g : G), g * n * g⁻¹ ∈ s
This theorem states that, for any given group `G` and a subset `s` of `G`, if `s` is a normal subgroup, then it is closed under conjugation. More specifically, for every element `n` in `s` and any element `g` in `G`, the result of the operation `g * n * g⁻¹` (where `*` denotes the group operation and `g⁻¹` is the inverse of `g`) is also an element of `s`. This property is characteristic of normal subgroups in group theory.
More concisely: In a group, if a subset is a normal subgroup, then it is closed under conjugation, that is, for all elements g in the group and n in the subset, g * n * g⁻¹ is also in the subset.
|