KleinFour

📁 Source: Mathlib/GroupTheory/SpecificGroups/KleinFour.lean

Statistics

Metric	Count
Definitions IsAddKleinFour, addEquiv, addEquiv', IsKleinFour, mulEquiv, mulEquiv'	6
Theorems add_self, card_four, card_four', eq_add_of_ne_all, eq_finset_univ, exponent_two, instFinite, neg_eq_self, nonempty_addEquiv, not_isAddCyclic, card_four, card_four', eq_finset_univ, eq_mul_of_ne_all, exponent_two, instFinite, inv_eq_self, mul_self, nonempty_mulEquiv, not_isCyclic, instIsAddKleinFourAdditiveOfIsKleinFour, instIsAddKleinFourProdZModOfNatNat, instIsKleinFourMultiplicativeOfIsAddKleinFour	23
Total	29

IsAddKleinFour

Definitions

Name	Category	Theorems
addEquiv 📖	CompOp	—
addEquiv' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_self 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	add_eq_zero_iff_eq_neg neg_eq_self
card_four 📖	mathematical	—	Nat.card	—	—
card_four' 📖	mathematical	—	Fintype.card	—	card_four Nat.card_eq_fintype_card
eq_add_of_ne_all 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	instFinite Finset.eq_of_mem_insert_of_notMem Finset.mem_univ eq_finset_univ Finset.mem_insert Finset.mem_singleton
eq_finset_univ 📖	mathematical	—	Finset Finset.instInsert AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Finset.instSingleton NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Finset.univ	—	Finset.eq_univ_of_card card_four' Finset.card_insert_of_notMem Finset.mem_insert add_eq_left AddLeftCancelSemigroup.toIsLeftCancelAdd add_eq_right AddRightCancelSemigroup.toIsRightCancelAdd Finset.mem_singleton Set.mem_insert_iff Set.mem_singleton_iff add_notMem_of_exponent_two exponent_two Finset.card_singleton
exponent_two 📖	mathematical	—	AddMonoid.exponent SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	—
instFinite 📖	mathematical	—	Finite	—	Nat.finite_of_card_ne_zero card_four Nat.instAtLeastTwoHAddOfNat OfNat.ofNat_ne_zero Nat.instCharZero
neg_eq_self 📖	mathematical	—	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	neg_eq_self_of_exponent_two exponent_two
nonempty_addEquiv 📖	mathematical	—	AddEquiv AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	instFinite card_four' Equiv.setValue_eq
not_isAddCyclic 📖	mathematical	—	IsAddCyclic SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	exponent_two card_four IsAddCyclic.exponent_eq_card

IsKleinFour

Definitions

Name	Category	Theorems
mulEquiv 📖	CompOp	—
mulEquiv' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_four 📖	mathematical	—	Nat.card	—	—
card_four' 📖	mathematical	—	Fintype.card	—	card_four Nat.card_eq_fintype_card
eq_finset_univ 📖	mathematical	—	Finset Finset.instInsert MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Finset.instSingleton InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Finset.univ	—	Finset.eq_univ_of_card card_four' Finset.card_insert_of_notMem LeftCancelSemigroup.toIsLeftCancelMul RightCancelSemigroup.toIsRightCancelMul mul_notMem_of_exponent_two exponent_two Finset.card_singleton
eq_mul_of_ne_all 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	instFinite Finset.eq_of_mem_insert_of_notMem Finset.mem_univ eq_finset_univ
exponent_two 📖	mathematical	—	Monoid.exponent DivInvMonoid.toMonoid Group.toDivInvMonoid	—	—
instFinite 📖	mathematical	—	Finite	—	Nat.finite_of_card_ne_zero card_four Nat.instCharZero Nat.instAtLeastTwoHAddOfNat
inv_eq_self 📖	mathematical	—	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	inv_eq_self_of_exponent_two exponent_two
mul_self 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	mul_eq_one_iff_eq_inv inv_eq_self
nonempty_mulEquiv 📖	mathematical	—	MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	instFinite card_four' Equiv.setValue_eq
not_isCyclic 📖	mathematical	—	IsCyclic DivInvMonoid.toZPow Group.toDivInvMonoid	—	exponent_two card_four IsCyclic.exponent_eq_card

(root)

Definitions

Name	Category	Theorems
IsAddKleinFour 📖	CompData	2 math math: instIsAddKleinFourAdditiveOfIsKleinFour, instIsAddKleinFourProdZModOfNatNat
IsKleinFour 📖	CompData	3 math math: alternatingGroup.kleinFour_isKleinFour, DihedralGroup.instIsKleinFourOfNatNat, instIsKleinFourMultiplicativeOfIsAddKleinFour

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsAddKleinFourAdditiveOfIsKleinFour 📖	mathematical	—	IsAddKleinFour Additive Additive.addGroup	—	IsKleinFour.card_four IsKleinFour.exponent_two
instIsAddKleinFourProdZModOfNatNat 📖	mathematical	—	IsAddKleinFour ZMod Prod.instAddGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing	—	Nat.card_eq_fintype_card Fintype.card_prod ZMod.card AddMonoid.exponent_prod ZMod.exponent lcm_same normalize_eq Unique.instSubsingleton
instIsKleinFourMultiplicativeOfIsAddKleinFour 📖	mathematical	—	IsKleinFour Multiplicative Multiplicative.group	—	IsAddKleinFour.card_four IsAddKleinFour.exponent_two

---

← Back to Index