Pow

📁 Source: Mathlib/LinearAlgebra/SModEq/Pow.lean

Statistics

Metric	Count
Definitions	0
Theorems pow_add_one, pow_mul_of_le, pow_pow_add_one	3
Total	3

SModEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pow_add_one 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing SModEq Ring.toAddCommGroup Submodule.instPowNat IsScalarTower.right Algebra.id	SModEq CommRing.toRing Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Ideal Submodule.instPowNat IsScalarTower.right Algebra.id Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	IsScalarTower.right pow_mul_of_le Ideal.pow_le_self
pow_mul_of_le 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing SModEq Ring.toAddCommGroup Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder	SModEq CommRing.toRing Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Ideal Submodule.mul IsScalarTower.right Algebra.id Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Ideal.instIsTwoSided_1 idealQuotientMk mono IsScalarTower.right sub_mem Commute.mul_neg_geom_sum₂ Commute.all Ideal.mul_mem_mul map_natCast RingHom.instRingHomClass Ideal.Quotient.eq_zero_iff_mem map_sum RingHomClass.toAddMonoidHomClass Finset.sum_congr map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Finset.sum_const Finset.card_range nsmul_eq_mul MulZeroClass.zero_mul
pow_pow_add_one 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing SModEq Ring.toAddCommGroup	SModEq CommRing.toRing Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Ideal Submodule.instPowNat IsScalarTower.right Algebra.id Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid	—	IsScalarTower.right zero_add pow_one pow_zero pow_succ pow_mul pow_add_one

---

← Back to Index