Pow

📁 Source: Mathlib/Algebra/Order/Ring/Pow.lean

Statistics

Metric	Count
Definitions	0
Theorems pow_add_mul_le_add_pow, pow_add_mul_le_add_pow_of_sq_nonneg, one_add_le_pow_of_two_add_nonneg, one_add_mul_le_pow, one_add_mul_le_pow', one_add_mul_le_pow_of_sq_nonneg, one_add_mul_sub_le_pow, pow_add_mul_le_add_pow, pow_add_mul_le_add_pow_of_sq_nonneg	9
Total	9

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pow_add_mul_le_add_pow 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Distrib.toAdd instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.instAtLeastTwoHAddOfNat	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Nat.instAtLeastTwoHAddOfNat pow_add_mul_le_add_pow_of_sq_nonneg sq_nonneg IsOrderedRing.toPosMulMono IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid
pow_add_mul_le_add_pow_of_sq_nonneg 📖	—	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	—	Nat.instAtLeastTwoHAddOfNat pow_zero Nat.cast_zero zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub mul_one MulZeroClass.zero_mul add_zero pow_one Nat.cast_one tsub_self one_mul le_add_of_nonneg_right IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid sq two_mul add_mul Distrib.rightDistribClass eq add_assoc mul_add Distrib.leftDistribClass add_nonneg mul_nonneg IsOrderedRing.toPosMulMono Nat.cast_nonneg zero_le_one IsOrderedRing.toZeroLEOneClass pow_nonneg pow_succ' Nat.cast_add two_add_one_eq_three mul_assoc pow_left left_comm symm Nat.cast_commute Mathlib.Tactic.Abel.subst_into_add Mathlib.Tactic.Abel.term_atom Mathlib.Tactic.Abel.term_add_term Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat zero_add Mathlib.Tactic.Abel.term_add_const Mathlib.Tactic.Abel.const_add_term mul_le_mul_of_nonneg_left

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
one_add_le_pow_of_two_add_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.instAtLeastTwoHAddOfNat	AddMonoidWithOne.toOne Distrib.toMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Nat.instAtLeastTwoHAddOfNat one_add_mul_le_pow_of_sq_nonneg sq_nonneg IsOrderedRing.toPosMulMono IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid
one_add_mul_le_pow 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.instAtLeastTwoHAddOfNat	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne Distrib.toMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	Nat.instAtLeastTwoHAddOfNat one_add_le_pow_of_two_add_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE neg_le_iff_add_nonneg' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid
one_add_mul_le_pow' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Nat.instAtLeastTwoHAddOfNat one_add_mul_le_pow_of_sq_nonneg sq
one_add_mul_le_pow_of_sq_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat	Distrib.toMul	—	Nat.instAtLeastTwoHAddOfNat one_pow mul_one Commute.pow_add_mul_le_add_pow_of_sq_nonneg Commute.one_left zero_le_one IsOrderedRing.toZeroLEOneClass
one_add_mul_sub_le_pow 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toMul AddMonoidWithOne.toNatCast SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	Nat.instAtLeastTwoHAddOfNat one_add_one_eq_two neg_add sub_eq_add_neg sub_le_sub_iff_right covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing add_sub_cancel one_add_mul_le_pow
pow_add_mul_le_add_pow 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Distrib.toMul instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.instAtLeastTwoHAddOfNat	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Nat.instAtLeastTwoHAddOfNat Commute.pow_add_mul_le_add_pow Commute.all
pow_add_mul_le_add_pow_of_sq_nonneg 📖	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Distrib.toMul instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	—	Nat.instAtLeastTwoHAddOfNat Commute.pow_add_mul_le_add_pow_of_sq_nonneg Commute.all

---

← Back to Index