Group

📁 Source: Mathlib/Tactic/Group.lean

Statistics

Metric	Count
Definitions aux_group₁, aux_group₂, group	3
Theorems zpow_trick, zpow_trick_one, zpow_trick_one', zsmul_trick, zsmul_trick_zero, zsmul_trick_zero'	6
Total	9

Mathlib.Tactic.Group

Definitions

Name	Category	Theorems
aux_group₁ 📖	CompOp	—
aux_group₂ 📖	CompOp	—
group 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
zpow_trick 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid DivInvMonoid.toZPow	—	mul_assoc zpow_add
zpow_trick_one 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid DivInvMonoid.toZPow	—	mul_assoc mul_self_zpow
zpow_trick_one' 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid DivInvMonoid.toZPow	—	mul_assoc mul_zpow_self
zsmul_trick 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SubNegMonoid.toZSMul	—	add_assoc add_zsmul
zsmul_trick_zero 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SubNegMonoid.toZSMul	—	add_assoc add_zsmul_self
zsmul_trick_zero' 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SubNegMonoid.toZSMul	—	add_assoc add_self_zsmul

---

← Back to Index