Structures · Algebra
IsAddKleinFour
An (additive) Klein four-group is an (additive) group of cardinality four and exponent two.
- Shape
- One type argument · adds card_four, exponent_two
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Prod
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by14
- IsAddKleinFour.exponent_two
- IsAddKleinFour.card_four'
- IsAddKleinFour.card_four
- IsAddKleinFour.addEquiv
- IsAddKleinFour.neg_eq_self
- IsAddKleinFour.eq_finset_univ
- IsAddKleinFour.not_isAddCyclic
- IsAddKleinFour.instFinite
- IsAddKleinFour.isAddCommutative
- instIsKleinFourMultiplicativeOfIsAddKleinFour
- IsAddKleinFour.add_self
- IsAddKleinFour.eq_add_of_ne_all
- IsAddKleinFour.nonempty_addEquiv
- IsAddKleinFour.addEquiv'
Ancestors0
No ancestors.