NatPowAssoc

📁 Source: Mathlib/Algebra/Group/NatPowAssoc.lean

Statistics

Metric	Count
Definitions NatPowAssoc	1
Theorems cast_npow, PowAssoc, cast_npow, npow_add, npow_one, npow_zero, instNatPowAssoc, instNatPowAssoc, neg_npow_assoc, npow_add, npow_mul, npow_mul', npow_mul_assoc, npow_mul_comm, npow_one, npow_zero	16
Total	17

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_npow 📖	mathematical	—	NonAssocRing.toIntCast Monoid.toNatPow instMonoid AddGroupWithOne.toIntCast AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne	—	pow_zero npow_zero cast_one npow_add Monoid.PowAssoc npow_one cast_mul

Monoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
PowAssoc 📖	mathematical	—	NatPowAssoc toMulOneClass toNatPow	—	pow_add pow_zero pow_one

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_npow 📖	mathematical	—	AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Monoid.toNatPow instMonoid	—	pow_zero cast_one npow_zero npow_add Monoid.PowAssoc cast_mul npow_one

NatPowAssoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
npow_add 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne	—	—
npow_one 📖	—	—	—	—	—
npow_zero 📖	mathematical	—	MulOne.toOne MulOneClass.toMulOne	—	—

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNatPowAssoc 📖	mathematical	NatPowAssoc	mulOneClass instPow	—	npow_add npow_zero npow_one

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNatPowAssoc 📖	mathematical	—	NatPowAssoc instMulOneClass instPow	—	npow_add npow_zero npow_one

(root)

Definitions

Name	Category	Theorems
NatPowAssoc 📖	CompData	2 math math: Prod.instNatPowAssoc, Monoid.PowAssoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
neg_npow_assoc 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocRing.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne	—	npow_zero one_mul npow_add npow_one neg_mul_comm mul_one neg_mul
npow_add 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne	—	NatPowAssoc.npow_add
npow_mul 📖	—	—	—	—	npow_zero mul_add Distrib.leftDistribClass npow_add mul_one npow_one
npow_mul' 📖	—	—	—	—	mul_comm npow_mul
npow_mul_assoc 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne	—	add_assoc
npow_mul_comm 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne	—	add_comm
npow_one 📖	—	—	—	—	NatPowAssoc.npow_one
npow_zero 📖	mathematical	—	MulOne.toOne MulOneClass.toMulOne	—	NatPowAssoc.npow_zero

---

← Back to Index