AddSubgroup.fg_iff_addSubmonoid_fg
theorem AddSubgroup.fg_iff_addSubmonoid_fg : ∀ {G : Type u_3} [inst : AddGroup G] (P : AddSubgroup G), P.FG ↔ P.FG := by
sorry
This theorem states that for any additive subgroup `P` of a group `G`, `P` is finitely generated as an additive subgroup if and only if it is finitely generated as an additive submonoid. In other words, `P` is the closure of a finite subset of `G` both when considered as a subgroup and a submonoid.
More concisely: A subgroup `P` of a group `G` is finitely generated as an additive subgroup if and only if it is finitely generated as an additive submonoid.
|
Group.rank_le
theorem Group.rank_le :
∀ (G : Type u_3) [inst : Group G] [h : Group.FG G] {S : Finset G},
Subgroup.closure ↑S = ⊤ → Group.rank G ≤ S.card
The theorem `Group.rank_le` states that for any finitely generated group `G`, if the `Subgroup` generated by a finite set `S` of elements in `G` equals the entire group (`⊤`), then the rank of the group `G` (i.e., the minimum number of generators required to generate `G`) is less than or equal to the cardinality of the set `S`.
More concisely: If a finitely generated group `G` is equal to the subgroup generated by a finite set `S` of elements in `G`, then the rank of `G` is less than or equal to the cardinality of `S`.
|
AddGroup.fg_iff_addMonoid_fg
theorem AddGroup.fg_iff_addMonoid_fg : ∀ {G : Type u_3} [inst : AddGroup G], AddGroup.FG G ↔ AddMonoid.FG G
This theorem states that for any given type `G`, if `G` is an additive group, then `G` is finitely generated if and only if it is finitely generated as an additive monoid. In mathematical terms, it's stating that the properties of being finitely generated in the contexts of additive groups and additive monoids are equivalent for a given type.
More concisely: For an additive group `G`, it is finitely generated if and only if it is finitely generated as an additive monoid.
|
Group.fg_iff
theorem Group.fg_iff : ∀ {G : Type u_3} [inst : Group G], Group.FG G ↔ ∃ S, Subgroup.closure S = ⊤ ∧ S.Finite := by
sorry
This theorem provides an equivalent characterization of a finitely generated group. In the context of a group `G`, the theorem states that `G` is finitely generated (denoted by `Group.FG G`) if and only if there exists a set `S` such that the subgroup generated by `S` is the whole group (`Subgroup.closure S = ⊤`) and `S` is a finite set (`S.Finite`).
More concisely: A group is finitely generated if and only if there exists a finite set generating the entire group.
|
Monoid.fg_of_surjective
theorem Monoid.fg_of_surjective :
∀ {M : Type u_1} [inst : Monoid M] {M' : Type u_3} [inst_1 : Monoid M'] [inst_2 : Monoid.FG M] (f : M →* M'),
Function.Surjective ⇑f → Monoid.FG M'
The theorem `Monoid.fg_of_surjective` states that for all types `M` and `M'` where `M` and `M'` are monoids (i.e., they satisfy the algebraic structure of a monoid), and where `M` is finitely generated (notated as `Monoid.FG M`), if there exists a surjective (onto) monoid homomorphism `f` from `M` to `M'` (notated as `f : M →* M'`), then `M'` is also finitely generated. In other words, the surjectivity of a monoid homomorphism from a finitely generated monoid guarantees that the codomain is also finitely generated.
More concisely: If `M` is a finitely generated monoid and there exists a surjective monoid homomorphism from `M` to `M'`, then `M'` is also finitely generated.
|
AddMonoid.fg_def
theorem AddMonoid.fg_def : ∀ {N : Type u_2} [inst : AddMonoid N], AddMonoid.FG N ↔ ⊤.FG
The theorem `AddMonoid.fg_def` states that for any type `N` that is an instance of `AddMonoid`, it is finitely generated (abbreviated as `FG`) if and only if its additive submonoid is also finitely generated. In other words, an additive monoid is finitely generated iff its top additive submonoid (denoted as `⊤`) is finitely generated. This theorem connects the concepts of a finitely generated monoid and a finitely generated submonoid in the context of additive monoids.
More concisely: An additive monoid is finitely generated if and only if its top additive submonoid is finitely generated.
|
AddGroup.fg_iff
theorem AddGroup.fg_iff :
∀ {G : Type u_3} [inst : AddGroup G], AddGroup.FG G ↔ ∃ S, AddSubgroup.closure S = ⊤ ∧ S.Finite
This theorem provides an equivalent formulation for the finitely generated property of an additive group. Specifically, an additive group `G` is said to be finitely generated (denoted by `AddGroup.FG G`) if and only if there exists a set `S` such that the additive subgroup generated by `S` is the entire group (`AddSubgroup.closure S = ⊤`) and `S` is a finite set (`S.Finite`). In other words, we can generate the whole group using a finite set of elements and the group operation of addition.
More concisely: An additive group is finitely generated if and only if there exists a finite set generating the whole group through addition.
|
AddMonoid.fg_iff
theorem AddMonoid.fg_iff :
∀ {M : Type u_1} [inst : AddMonoid M], AddMonoid.FG M ↔ ∃ S, AddSubmonoid.closure S = ⊤ ∧ S.Finite
The theorem `AddMonoid.fg_iff` states that for any type `M` equipped with an additive monoid structure, the `AddMonoid` is finitely generated (`AddMonoid.FG M`) if and only if there exists a set `S` such that the `AddSubmonoid` generated by `S` equals the entirety of the `AddMonoid` (symbolically, `AddSubmonoid.closure S = ⊤`) and `S` is finite. This theorem provides an alternative characterization of finitely generated additive monoids using the notion of finite sets (`Set.Finite`) instead of finite subsets (`Finset`).
More concisely: A type equipped with an additive monoid structure is finitely generated if and only if there exists a finite set generating the entire additive monoid.
|
AddSubmonoid.fg_iff
theorem AddSubmonoid.fg_iff :
∀ {M : Type u_1} [inst : AddMonoid M] (P : AddSubmonoid M), P.FG ↔ ∃ S, AddSubmonoid.closure S = P ∧ S.Finite := by
sorry
This theorem provides an equivalent formulation of the property of an additive submonoid being finitely generated (`AddSubmonoid.FG`). It states that for any additive monoid `M`, an additive submonoid `P` of `M` is finitely generated if and only if there exists a set `S` such that `P` is the additive submonoid generated by `S` (`AddSubmonoid.closure S = P`) and `S` is a finite set (`Set.Finite S`).
More concisely: An additive submonoid of an abelian group is finitely generated if and only if it can be generated by a finite set.
|
Monoid.fg_iff
theorem Monoid.fg_iff : ∀ {M : Type u_1} [inst : Monoid M], Monoid.FG M ↔ ∃ S, Submonoid.closure S = ⊤ ∧ S.Finite := by
sorry
This theorem states that for any type `M` equipped with a `Monoid` structure, `M` is finitely generated as a monoid (denoted by `Monoid.FG M`) if and only if there exists a set `S` such that the submonoid generated by `S` is the whole monoid (`Submonoid.closure S = ⊤`) and `S` is a finite set (`S.Finite`). In the context of algebra, a monoid is said to be finitely generated if there is a finite set of elements from which all elements of the monoid can be obtained using just the monoid operations.
More concisely: A monoid `M` is finitely generated if and only if there exists a finite set `S` that generates `M`, i.e., `M` is equal to the submonoid generated by `S`.
|
Group.rank_spec
theorem Group.rank_spec :
∀ (G : Type u_3) [inst : Group G] [h : Group.FG G], ∃ S, S.card = Group.rank G ∧ Subgroup.closure ↑S = ⊤
The theorem `Group.rank_spec` states that for any group `G` that is finitely generated (`Group.FG G`), there exists a set `S` such that the cardinality of `S` is equal to the rank of the group (the minimum number of generators of the group as described by `Group.rank G`) and the closure of `S` (i.e., the smallest subgroup of `G` containing all elements of `S` as given by `Subgroup.closure ↑S`) is the entire group `G` (denoted by `⊤`). In other words, `S` is a set of generators for the group `G` and it is of minimal size.
More concisely: For any finitely generated group $G$, there exists a set $S$ of generators for $G$ such that $S$ is of minimum size and the subgroup generated by $S$ is equal to $G$ (i.e., $S$ is a generating set of minimum cardinality for $G$).
|
Monoid.fg_iff_add_fg
theorem Monoid.fg_iff_add_fg : ∀ {M : Type u_1} [inst : Monoid M], Monoid.FG M ↔ AddMonoid.FG (Additive M)
This theorem, `Monoid.fg_iff_add_fg`, states that for any type `M` that has a `Monoid` structure, `M` is finitely generated as a monoid if and only if the additive version of `M` (i.e., `Additive M`), which carries the corresponding additive monoid structure, is finitely generated as an additive monoid. In other words, the theorem establishes an equivalence between the finite generation of the multiplicative structure on `M` and the finite generation of the associated additive structure on `Additive M`.
More concisely: For any type `M` with a `Monoid` structure, `M` is finitely generated as a monoid if and only if `Additive M` is finitely generated as an additive monoid.
|
AddGroup.fg_def
theorem AddGroup.fg_def : ∀ {H : Type u_4} [inst : AddGroup H], AddGroup.FG H ↔ ⊤.FG
The theorem `AddGroup.fg_def` states that for any type `H` that has an additive group structure, `H` is finitely generated as an additive group if and only if the whole additive group `⊤` is a finitely generated subgroup. In simpler terms, an additive group `H` is said to be finitely generated when there exists a finite subset of `H` whose additive closure generates the entire group, and this matches up with the property of `⊤` being a finitely generated subgroup of `H`.
More concisely: An additive group H is finitely generated if and only if the whole additive group ⊤ is a finitely generated subgroup of H.
|
Subgroup.fg_iff_submonoid_fg
theorem Subgroup.fg_iff_submonoid_fg : ∀ {G : Type u_3} [inst : Group G] (P : Subgroup G), P.FG ↔ P.FG
The theorem `Subgroup.fg_iff_submonoid_fg` states that for any group `G`, a subgroup `P` of `G` is finitely generated if and only if `P` is finitely generated when considered as a submonoid. Here, a subgroup (or submonoid) is finitely generated if it can be expressed as the closure of a finite subset of the group (or monoid).
More concisely: A subgroup of a group is finitely generated if and only if considered as a submonoid, it is finitely generated.
|
Monoid.fg_iff_submonoid_fg
theorem Monoid.fg_iff_submonoid_fg : ∀ {M : Type u_1} [inst : Monoid M] (N : Submonoid M), Monoid.FG ↥N ↔ N.FG := by
sorry
This theorem states that for any monoid `M` and any submonoid `N` of `M`, `N` is finitely generated as a monoid if and only if `N` is finitely generated as a submonoid of `M`. In other words, the property of being finitely generated is preserved whether we consider `N` as a monoid in its own right or as a submonoid of `M`.
More concisely: For any monoid `M` and its submonoid `N`, `N` is finitely generated as a monoid if and only if it is finitely generated as a submonoid of `M`.
|
Submonoid.fg_iff
theorem Submonoid.fg_iff :
∀ {M : Type u_1} [inst : Monoid M] (P : Submonoid M), P.FG ↔ ∃ S, Submonoid.closure S = P ∧ S.Finite
This theorem states that a submonoid `P` of a monoid `M` is finitely generated (as per the definition of `Submonoid.FG`) if and only if there exists a set `S` such that `S` is the generating set of `P` (i.e., the submonoid closure of `S` is `P`) and `S` is a finite set. In other words, a submonoid is finitely generated if it can be created by the closure operation on a finite set of elements.
More concisely: A submonoid of a monoid is finitely generated if and only if it can be generated by a finite set.
|
Subgroup.fg_iff
theorem Subgroup.fg_iff :
∀ {G : Type u_3} [inst : Group G] (P : Subgroup G), P.FG ↔ ∃ S, Subgroup.closure S = P ∧ S.Finite
The theorem `Subgroup.fg_iff` states that for any group `G` and any subgroup `P` of `G`, `P` is a finitely generated (FG) subgroup if and only if there exists a set `S` such that `P` is the subgroup generated by `S` and `S` is a finite set. Here, `Subgroup.closure S` denotes the subgroup generated by the set `S`, and the term `S.Finite` asserts that `S` is a finite set.
More concisely: A subgroup of a group is finitely generated if and only if it can be generated by a finite set.
|
AddSubgroup.fg_iff
theorem AddSubgroup.fg_iff :
∀ {G : Type u_3} [inst : AddGroup G] (P : AddSubgroup G), P.FG ↔ ∃ S, AddSubgroup.closure S = P ∧ S.Finite := by
sorry
This theorem states that for any additive group `G` and any subgroup `P` of `G`, `P` is finitely generated (`P.FG`) if and only if there exists a set `S` such that the subgroup generated by `S` is `P` and `S` is a finite set. This provides an equivalent expression of the property of being finitely generated in terms of finite sets instead of finite subsets (`Finset`).
More concisely: A subgroup of an additive group is finitely generated if and only if it can be generated by a finite set.
|
Group.fg_iff_monoid_fg
theorem Group.fg_iff_monoid_fg : ∀ {G : Type u_3} [inst : Group G], Group.FG G ↔ Monoid.FG G
This theorem states that for every type `G` that has a group structure, `G` is finitely generated as a group if and only if it is finitely generated as a monoid. In other words, the property of a group being finitely generated does not depend on the existence of inverse elements, but solely on the closure property and associativity, which are the defining properties of a monoid.
More concisely: A group is finitely generated if and only if it is finitely generated as a monoid.
|