Pow

📁 Source: Mathlib/Tactic/NormNum/Pow.lean

Statistics

Metric	Count
Definitions IsNatPowT, evalIntPow, evalNatPow, evalPow, core, evalZPow	6
Theorems bit0, bit1, run, run', trans, intPow_negOfNat_bit0, intPow_negOfNat_bit1, intPow_ofNat, isInt_pow, isInt_zpow_neg, isInt_zpow_pos, isNNRat_pow, isNNRat_zpow_neg, isNNRat_zpow_pos, isNat_pow, isNat_zpow_neg, isNat_zpow_pos, isRat_pow, isRat_zpow_neg, isRat_zpow_pos, natPow_one, natPow_zero, one_natPow, zero_natPow	24
Total	30

Mathlib.Meta.NormNum

Definitions

Name	Category	Theorems
IsNatPowT 📖	CompData	2 math math: IsNatPowT.bit1, IsNatPowT.bit0
evalIntPow 📖	CompOp	—
evalNatPow 📖	CompOp	—
evalPow 📖	CompOp	—
evalZPow 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
intPow_negOfNat_bit0 📖	—	—	—	—	Int.pow_eq pow_mul neg_pow_two Nat.instAtLeastTwoHAddOfNat two_mul pow_add Nat.cast_mul Nat.cast_pow
intPow_negOfNat_bit1 📖	—	—	—	—	Int.pow_eq pow_succ pow_mul neg_pow_two Nat.instAtLeastTwoHAddOfNat two_mul pow_add mul_neg mul_comm mul_left_comm Nat.cast_mul Nat.cast_pow
intPow_ofNat 📖	—	—	—	—	Nat.cast_pow
isInt_pow 📖	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring IsInt IsNat Nat.instAddMonoidWithOne	—	—	Int.cast_pow
isInt_zpow_neg 📖	mathematical	IsInt Int.instRing DivisionRing.toRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring	DivInvMonoid.toZPow DivisionRing.toDivInvMonoid	—	IsInt.out Int.cast_negOfNat zpow_neg zpow_natCast
isInt_zpow_pos 📖	mathematical	IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing IsInt DivisionRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring	DivInvMonoid.toZPow DivisionRing.toDivInvMonoid	—	IsNat.out zpow_natCast
isNNRat_pow 📖	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsNNRat IsNat Nat.instAddMonoidWithOne	—	—	Nat.cast_pow Commute.mul_pow Invertible.congr invOf_pow
isNNRat_zpow_neg 📖	mathematical	IsInt Int.instRing IsNNRat DivisionSemiring.toSemiring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid	—	IsInt.out Int.cast_negOfNat zpow_neg zpow_natCast
isNNRat_zpow_pos 📖	mathematical	IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing IsNNRat DivisionSemiring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	IsNat.out zpow_natCast
isNat_pow 📖	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsNat AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Nat.instAddMonoidWithOne	—	—	Nat.cast_pow
isNat_zpow_neg 📖	mathematical	IsInt Int.instRing IsNat AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid	—	IsInt.out Int.cast_negOfNat zpow_neg zpow_natCast
isNat_zpow_pos 📖	mathematical	IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	IsNat.out zpow_natCast
isRat_pow 📖	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring IsRat IsNat Nat.instAddMonoidWithOne	—	—	Nat.cast_pow Commute.mul_pow Int.cast_pow Invertible.congr invOf_pow
isRat_zpow_neg 📖	mathematical	IsInt Int.instRing IsRat DivisionRing.toRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring	DivInvMonoid.toZPow DivisionRing.toDivInvMonoid	—	IsInt.out Int.cast_negOfNat zpow_neg zpow_natCast
isRat_zpow_pos 📖	mathematical	IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing IsRat DivisionRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring	DivInvMonoid.toZPow DivisionRing.toDivInvMonoid	—	IsNat.out zpow_natCast
natPow_one 📖	—	—	—	—	—
natPow_zero 📖	—	—	—	—	—
one_natPow 📖	—	—	—	—	—
zero_natPow 📖	—	—	—	—	—

Mathlib.Meta.NormNum.IsNatPowT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bit0 📖	mathematical	—	Mathlib.Meta.NormNum.IsNatPowT	—	two_mul pow_add
bit1 📖	mathematical	—	Mathlib.Meta.NormNum.IsNatPowT	—	two_mul pow_add pow_one mul_assoc
run 📖	—	Mathlib.Meta.NormNum.IsNatPowT	—	—	run'
run' 📖	—	Mathlib.Meta.NormNum.IsNatPowT	—	—	—
trans 📖	—	Mathlib.Meta.NormNum.IsNatPowT	—	—	run'

Mathlib.Meta.NormNum.evalPow

Definitions

Name	Category	Theorems
core 📖	CompOp	—

---

← Back to Index