Documentation Verification Report

Quaternion

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

Statistics

Metric	Count
Definitions `QuaternionGroup`, `instFintypeOfNeZeroNat`, `instGroup`, `instInhabited`, `quaternionGroupZeroEquivDihedralGroupZero`, `instDecidableEqQuaternionGroup`, `decEq`	7
Theorems `a_mul_a`, `a_mul_xa`, `a_one_pow`, `a_one_pow_n`, `a_zero`, `card`, `exponent`, `instNontrivial`, `one_def`, `orderOf_a`, `orderOf_a_one`, `orderOf_xa`, `quaternionGroup_one_isCyclic`, `xa_mul_a`, `xa_mul_xa`, `xa_pow_four`, `xa_sq`	17
Total	24

QuaternionGroup

Definitions

Name	Category	Theorems
`instFintypeOfNeZeroNat` 📖	CompOp	1 math math: `card`
`instGroup` 📖	CompOp	15 math math: `a_one_pow_n`, `orderOf_a_one`, `a_mul_xa`, `quaternionGroup_one_isCyclic`, `a_mul_a`, `xa_mul_a`, `one_def`, `orderOf_xa`, `orderOf_a`, `a_one_pow`, `xa_mul_xa`, `xa_sq`, `a_zero`, `exponent`, `xa_pow_four`
`instInhabited` 📖	CompOp	—
`quaternionGroupZeroEquivDihedralGroupZero` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`a_mul_a` 📖	mathematical	—	`QuaternionGroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `a` `ZMod` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing`	—	—
`a_mul_xa` 📖	mathematical	—	`QuaternionGroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `a` `xa` `ZMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing`	—	—
`a_one_pow` 📖	mathematical	—	`QuaternionGroup` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `a` `ZMod` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing` `AddMonoidWithOne.toNatCast`	—	`Nat.cast_zero` `pow_succ` `a_mul_a` `Nat.cast_one`
`a_one_pow_n` 📖	mathematical	—	`QuaternionGroup` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `a` `ZMod` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`a_one_pow` `CharP.cast_eq_zero` `ZMod.charP` `a_zero`
`a_zero` 📖	mathematical	—	`a` `ZMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `QuaternionGroup` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroup`	—	—
`card` 📖	mathematical	—	`Fintype.card` `QuaternionGroup` `instFintypeOfNeZeroNat`	—	`Fintype.card_eq` `Fintype.card_sum` `ZMod.card` `Nat.instAtLeastTwoHAddOfNat` `two_mul` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul`
`exponent` 📖	mathematical	—	`Monoid.exponent` `QuaternionGroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `GCDMonoid.lcm` `Nat.instCommMonoidWithZero` `instGCDMonoidNat`	—	`Unique.instSubsingleton` `normalize_eq` `lcm_mul_left` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_ofNat` `eq_zero_or_neZero` `MulZeroClass.mul_zero` `GCDMonoid.lcm_zero_left` `Monoid.exponent_eq_zero_of_order_zero` `orderOf_a_one` `Monoid.exponent_dvd_of_forall_pow_eq_one` `orderOf_dvd_iff_pow_eq_one` `orderOf_a` `dvd_lcm_left` `orderOf_xa` `dvd_lcm_right` `lcm_dvd` `Monoid.order_dvd_exponent`
`instNontrivial` 📖	mathematical	—	`Nontrivial` `QuaternionGroup`	—	—
`one_def` 📖	mathematical	—	`QuaternionGroup` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroup` `a` `ZMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing`	—	—
`orderOf_a` 📖	mathematical	—	`orderOf` `QuaternionGroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `a` `ZMod.val`	—	`ZMod.natCast_zmod_val` `a_one_pow` `orderOf_pow` `Finite.of_fintype` `orderOf_a_one`
`orderOf_a_one` 📖	mathematical	—	`orderOf` `QuaternionGroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `a` `ZMod` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing`	—	`eq_zero_or_neZero` `MulZeroClass.mul_zero` `one_def` `a_one_pow` `ZMod.charZero` `LT.lt.ne'` `LE.le.lt_or_eq` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `orderOf_dvd_of_pow_eq_one` `a_one_pow_n` `pow_orderOf_eq_one` `ZMod.val_natCast` `ZMod.val_eq_zero` `LT.lt.ne` `orderOf_pos` `Finite.of_fintype`
`orderOf_xa` 📖	mathematical	—	`orderOf` `QuaternionGroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `xa`	—	`orderOf_eq_prime_pow` `Nat.prime_two` `pow_one` `xa_sq` `ZMod.val_natCast` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `ZMod.val_zero` `xa_pow_four`
`quaternionGroup_one_isCyclic` 📖	mathematical	—	`IsCyclic` `QuaternionGroup` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `instGroup`	—	`isCyclic_of_orderOf_eq_card` `Finite.of_fintype` `Nat.card_eq_fintype_card` `card` `mul_one` `orderOf_xa`
`xa_mul_a` 📖	mathematical	—	`QuaternionGroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `xa` `a` `ZMod` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing`	—	—
`xa_mul_xa` 📖	mathematical	—	`QuaternionGroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `xa` `a` `ZMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne`	—	—
`xa_pow_four` 📖	mathematical	—	`QuaternionGroup` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `xa` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`pow_succ` `pow_zero` `one_mul` `add_sub_cancel_right` `add_sub_assoc` `sub_sub_cancel` `two_mul` `Nat.cast_add` `CharP.cast_eq_zero` `ZMod.charP` `a_zero`
`xa_sq` 📖	mathematical	—	`QuaternionGroup` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `xa` `a` `ZMod` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing`	—	`sq` `add_sub_cancel_right`

(root)

Definitions

Name	Category	Theorems
`QuaternionGroup` 📖	CompData	17 math math: `QuaternionGroup.a_one_pow_n`, `QuaternionGroup.orderOf_a_one`, `QuaternionGroup.a_mul_xa`, `QuaternionGroup.card`, `QuaternionGroup.quaternionGroup_one_isCyclic`, `QuaternionGroup.a_mul_a`, `QuaternionGroup.xa_mul_a`, `QuaternionGroup.one_def`, `QuaternionGroup.orderOf_xa`, `QuaternionGroup.orderOf_a`, `QuaternionGroup.instNontrivial`, `QuaternionGroup.a_one_pow`, `QuaternionGroup.xa_mul_xa`, `QuaternionGroup.xa_sq`, `QuaternionGroup.a_zero`, `QuaternionGroup.exponent`, `QuaternionGroup.xa_pow_four`
`instDecidableEqQuaternionGroup` 📖	CompOp	—

instDecidableEqQuaternionGroup

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

---

← Back to Index