Pow

📁 Source: Mathlib/Algebra/Regular/Pow.lean

Statistics

Metric	Count
Definitions	0
Theorems prod, prod, prod	3
Total	3

IsLeftRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod 📖	mathematical	IsLeftRegular MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	IsLeftRegular MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset.prod	—	Finset.prod_induction mul IsRegular.left isRegular_one

IsRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod 📖	mathematical	IsRegular MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	IsRegular MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset.prod	—	IsLeftRegular.prod left IsRightRegular.prod right

IsRightRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod 📖	mathematical	IsRightRegular MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	IsRightRegular MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset.prod	—	Finset.prod_induction mul IsRegular.right isRegular_one

---

← Back to Index