Dihedral

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

Statistics

Metric	Count
Definitions `DihedralGroup`, `instFintypeOfNeZeroNat`, `instGroup`, `instInhabited`, `oddCommuteEquiv`, `Dihedral`, `instDecidableEqDihedralGroup`, `decEq`	8
Theorems `card`, `card_commute_odd`, `card_conjClasses_odd`, `center_eq_bot_of_odd_ne_one`, `commutative_iff`, `exponent`, `instInfiniteOfNatNat`, `instIsKleinFourOfNatNat`, `instNontrivial`, `inv_r`, `inv_sr`, `isCyclic_iff`, `nat_card`, `not_commutative`, `not_isCyclic`, `oddCommuteEquiv_apply`, `oddCommuteEquiv_symm_apply`, `one_def`, `orderOf_r`, `orderOf_r_one`, `orderOf_sr`, `r_mul_r`, `r_mul_sr`, `r_one_pow`, `r_one_pow_n`, `r_one_zpow`, `r_pow`, `r_zero`, `r_zpow`, `sr_mul_r`, `sr_mul_self`, `sr_mul_sr`	32
Total	40

DihedralGroup

Definitions

Name	Category	Theorems
`instFintypeOfNeZeroNat` 📖	CompOp	1 math math: `card`
`instGroup` 📖	CompOp	32 math math: `r_one_zpow`, `orderOf_r`, `r_pow`, `exponent`, `card_commute_odd`, `commProb_nil`, `oddCommuteEquiv_symm_apply`, `oddCommuteEquiv_apply`, `orderOf_sr`, `orderOf_r_one`, `center_eq_bot_of_odd_ne_one`, `r_zpow`, `r_mul_r`, `instIsKleinFourOfNatNat`, `sr_mul_sr`, `isCyclic_iff`, `not_isCyclic`, `sr_mul_r`, `card_conjClasses_odd`, `commutative_iff`, `r_one_pow_n`, `one_def`, `commProb_odd`, `r_mul_sr`, `r_one_pow`, `inv_r`, `sr_mul_self`, `commProb_cons`, `r_zero`, `commProb_reciprocal`, `not_commutative`, `inv_sr`
`instInhabited` 📖	CompOp	—
`oddCommuteEquiv` 📖	CompOp	2 math math: `oddCommuteEquiv_symm_apply`, `oddCommuteEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card` 📖	mathematical	—	`Fintype.card` `DihedralGroup` `instFintypeOfNeZeroNat`	—	`Fintype.card_eq` `Fintype.card_sum` `ZMod.card` `Nat.instAtLeastTwoHAddOfNat` `two_mul`
`card_commute_odd` 📖	mathematical	`Odd` `Nat.instSemiring`	`Nat.card` `DihedralGroup` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup`	—	`LT.lt.ne'` `Odd.pos` `Nat.instCanonicallyOrderedAdd` `Nat.instNontrivial` `Nat.card_congr` `Nat.card_sum` `Finite.of_fintype` `Finite.instSum` `Finite.instProd` `Nat.card_prod` `Nat.card_zmod` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.mul_pf_left`
`card_conjClasses_odd` 📖	mathematical	`Odd` `Nat.instSemiring`	`Nat.card` `ConjClasses` `DihedralGroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup`	—	`Odd.pos` `Nat.instCanonicallyOrderedAdd` `Nat.instNontrivial` `card_commute_odd` `mul_comm` `card_comm_eq_card_conjClasses_mul_card` `nat_card` `Nat.instAtLeastTwoHAddOfNat` `mul_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `two_pos` `Nat.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`center_eq_bot_of_odd_ne_one` 📖	mathematical	`Odd` `Nat.instSemiring`	`Subgroup.center` `DihedralGroup` `instGroup` `Bot.bot` `Subgroup` `Subgroup.instBot`	—	`sub_self` `add_assoc` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `ZMod.add_self_eq_zero_iff_eq_zero` `NeZero.one` `ZMod.nontrivial`
`commutative_iff` 📖	mathematical	—	`DihedralGroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `not_commutative`
`exponent` 📖	mathematical	—	`Monoid.exponent` `DihedralGroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `GCDMonoid.lcm` `Nat.instCommMonoidWithZero` `instGCDMonoidNat`	—	`eq_zero_or_neZero` `Monoid.exponent_eq_zero_of_order_zero` `orderOf_r_one` `Monoid.exponent_dvd_of_forall_pow_eq_one` `orderOf_dvd_iff_pow_eq_one` `orderOf_r` `dvd_lcm_left` `orderOf_sr` `dvd_lcm_right` `lcm_dvd` `Monoid.order_dvd_exponent`
`instInfiniteOfNatNat` 📖	mathematical	—	`Infinite` `DihedralGroup`	—	`Equiv.infinite_iff` `Sum.infinite_of_right` `ZMod.infinite`
`instIsKleinFourOfNatNat` 📖	mathematical	—	`IsKleinFour` `DihedralGroup` `instGroup`	—	`nat_card` `exponent`
`instNontrivial` 📖	mathematical	—	`Nontrivial` `DihedralGroup`	—	—
`inv_r` 📖	mathematical	—	`DihedralGroup` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroup` `r` `ZMod` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `ZMod.commRing`	—	—
`inv_sr` 📖	mathematical	—	`DihedralGroup` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroup` `sr`	—	—
`isCyclic_iff` 📖	mathematical	—	`IsCyclic` `DihedralGroup` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `instGroup`	—	`not_imp_not` `not_isCyclic` `isCyclic_of_prime_card` `Nat.fact_prime_two` `nat_card`
`nat_card` 📖	mathematical	—	`Nat.card` `DihedralGroup`	—	`Nat.card_eq_zero_of_infinite` `instInfiniteOfNatNat` `Nat.card_eq_fintype_card` `card`
`not_commutative` 📖	mathematical	—	`DihedralGroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup`	—	`zero_sub` `zero_add` `Nat.instAtLeastTwoHAddOfNat` `ZMod.val_two_eq_two_mod` `ZMod.val_eq_zero` `one_add_one_eq_two` `neg_eq_iff_add_eq_zero` `sr_mul_r` `r_mul_sr`
`not_isCyclic` 📖	mathematical	—	`IsCyclic` `DihedralGroup` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `instGroup`	—	`exponent` `lcm_same` `normalize_eq` `Unique.instSubsingleton` `Nat.card_eq_fintype_card` `card` `IsCyclic.exponent_eq_card` `not_commutative` `IsCyclic.commutative`
`oddCommuteEquiv_apply` 📖	mathematical	`Odd` `Nat.instSemiring`	`DFunLike.coe` `Equiv` `DihedralGroup` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `ZMod` `EquivLike.toFunLike` `Equiv.instEquivLike` `oddCommuteEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing`	—	—
`oddCommuteEquiv_symm_apply` 📖	mathematical	`Odd` `Nat.instSemiring`	`DFunLike.coe` `Equiv` `ZMod` `DihedralGroup` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `oddCommuteEquiv` `sr` `r` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Units` `Units.instInv` `ZMod.unitOfCoprime`	—	—
`one_def` 📖	mathematical	—	`DihedralGroup` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroup` `r` `ZMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing`	—	—
`orderOf_r` 📖	mathematical	—	`orderOf` `DihedralGroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `r` `ZMod.val`	—	`ZMod.natCast_zmod_val` `r_one_pow` `orderOf_pow` `Finite.of_fintype` `orderOf_r_one`
`orderOf_r_one` 📖	mathematical	—	`orderOf` `DihedralGroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `r` `ZMod` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing`	—	`eq_zero_or_neZero` `orderOf_eq_zero_iff'` `r_one_pow` `one_def` `ZMod.charZero` `LT.lt.ne'` `LE.le.lt_or_eq` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `orderOf_dvd_of_pow_eq_one` `r_one_pow_n` `pow_orderOf_eq_one` `ZMod.val_natCast` `ZMod.val_eq_zero` `LT.lt.ne` `orderOf_pos` `Finite.of_fintype`
`orderOf_sr` 📖	mathematical	—	`orderOf` `DihedralGroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `sr`	—	`orderOf_eq_prime` `Nat.fact_prime_two` `sq` `sr_mul_self`
`r_mul_r` 📖	mathematical	—	`DihedralGroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `r` `ZMod` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing`	—	—
`r_mul_sr` 📖	mathematical	—	`DihedralGroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `r` `sr` `ZMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing`	—	—
`r_one_pow` 📖	mathematical	—	`DihedralGroup` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `r` `ZMod` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing` `AddMonoidWithOne.toNatCast`	—	`r_pow` `one_mul`
`r_one_pow_n` 📖	mathematical	—	`DihedralGroup` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `r` `ZMod` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`r_pow` `CharP.cast_eq_zero` `ZMod.charP` `MulZeroClass.mul_zero`
`r_one_zpow` 📖	mathematical	—	`DihedralGroup` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `instGroup` `r` `ZMod` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing` `AddGroupWithOne.toIntCast`	—	`r_zpow` `one_mul`
`r_pow` 📖	mathematical	—	`DihedralGroup` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `r` `ZMod` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`pow_zero` `Nat.cast_zero` `MulZeroClass.mul_zero` `pow_add` `pow_one` `r_mul_r` `Nat.cast_add` `Nat.cast_one` `mul_add` `Distrib.leftDistribClass` `mul_one`
`r_zero` 📖	mathematical	—	`r` `ZMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `DihedralGroup` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroup`	—	—
`r_zpow` 📖	mathematical	—	`DihedralGroup` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `instGroup` `r` `ZMod` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`zpow_natCast` `r_pow` `Int.cast_natCast` `zpow_negSucc` `Nat.cast_add` `Nat.cast_one` `neg_mul_eq_mul_neg` `neg_add_rev` `Int.cast_negSucc`
`sr_mul_r` 📖	mathematical	—	`DihedralGroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `sr` `r` `ZMod` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing`	—	—
`sr_mul_self` 📖	mathematical	—	`DihedralGroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `sr` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`sub_self`
`sr_mul_sr` 📖	mathematical	—	`DihedralGroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `sr` `r` `ZMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing`	—	—

Quandle

Definitions

Name	Category	Theorems
`Dihedral` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`DihedralGroup` 📖	CompData	36 math math: `DihedralGroup.r_one_zpow`, `DihedralGroup.orderOf_r`, `DihedralGroup.card`, `DihedralGroup.r_pow`, `DihedralGroup.exponent`, `DihedralGroup.instNontrivial`, `DihedralGroup.card_commute_odd`, `DihedralGroup.commProb_nil`, `DihedralGroup.oddCommuteEquiv_symm_apply`, `DihedralGroup.instInfiniteOfNatNat`, `DihedralGroup.oddCommuteEquiv_apply`, `DihedralGroup.orderOf_sr`, `DihedralGroup.orderOf_r_one`, `DihedralGroup.center_eq_bot_of_odd_ne_one`, `DihedralGroup.r_zpow`, `DihedralGroup.nat_card`, `DihedralGroup.r_mul_r`, `DihedralGroup.instIsKleinFourOfNatNat`, `DihedralGroup.sr_mul_sr`, `DihedralGroup.isCyclic_iff`, `DihedralGroup.not_isCyclic`, `DihedralGroup.sr_mul_r`, `DihedralGroup.card_conjClasses_odd`, `DihedralGroup.commutative_iff`, `DihedralGroup.r_one_pow_n`, `DihedralGroup.one_def`, `DihedralGroup.commProb_odd`, `DihedralGroup.r_mul_sr`, `DihedralGroup.r_one_pow`, `DihedralGroup.inv_r`, `DihedralGroup.sr_mul_self`, `DihedralGroup.commProb_cons`, `DihedralGroup.r_zero`, `DihedralGroup.commProb_reciprocal`, `DihedralGroup.not_commutative`, `DihedralGroup.inv_sr`
`instDecidableEqDihedralGroup` 📖	CompOp	—

instDecidableEqDihedralGroup

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

---

← Back to Index