IsKleinFour.nonempty_mulEquiv
theorem IsKleinFour.nonempty_mulEquiv :
∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : Group G₁] [inst_1 : Group G₂] [inst_2 : IsKleinFour G₁]
[inst_3 : IsKleinFour G₂], Nonempty (G₁ ≃* G₂)
This theorem states that any two `IsKleinFour` groups are isomorphic. In other words, given two groups `G₁` and `G₂` that both possess the `IsKleinFour` property, there exists a nonempty multiplicative equivalence between `G₁` and `G₂`. This multiplicative equivalence is a bijective map preserving the group operation. In the context of group theory, isomorphism implies the two groups have the same structure, even though their elements may be different.
More concisely: Any two groups with the `IsKleinFour` property are isomorphic.
|
IsKleinFour.card_four'
theorem IsKleinFour.card_four' :
∀ {G : Type u_1} [inst : Group G] [inst_1 : Fintype G] [inst : IsKleinFour G], Fintype.card G = 4
The theorem `IsKleinFour.card_four'` asserts that for any type `G` which forms a group, has a finite number of elements (i.e., is a `Fintype`), and satisfies the property of being a Klein four-group (`IsKleinFour`), the cardinality (or number of elements) of `G` is always equal to 4. This is a property specific to Klein four-groups, which are known in abstract algebra to always consist of precisely four elements.
More concisely: A finite group with four elements and the property of being a Klein four-group has exactly 4 elements.
|
IsAddKleinFour.card_four'
theorem IsAddKleinFour.card_four' :
∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Fintype G] [inst : IsAddKleinFour G], Fintype.card G = 4
The theorem `IsAddKleinFour.card_four'` states that for any type `G` which is an additive group and admits the structure of a finite type, if `G` also has the structure of an additive Klein four-group, then the cardinality of `G` (i.e., the number of elements in `G`) is exactly 4. In mathematical terms, it says that an additive Klein four-group has exactly 4 elements.
More concisely: An additive Klein four-group is a finite type with exactly 4 elements.
|
IsAddKleinFour.nonempty_addEquiv
theorem IsAddKleinFour.nonempty_addEquiv :
∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : AddGroup G₁] [inst_1 : AddGroup G₂] [inst_2 : IsAddKleinFour G₁]
[inst_3 : IsAddKleinFour G₂], Nonempty (G₁ ≃+ G₂)
The theorem `IsAddKleinFour.nonempty_addEquiv` states that for any two additive Klein Four groups `G₁` and `G₂`, there is a non-empty Set of additive group isomorphisms between them. In other words, there is at least one isomorphism that preserves the additive group structure between any two Klein Four groups.
More concisely: For any two Klein Four groups, there exists an additive group isomorphism between them.
|