PowMod

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

Statistics

Metric	Count
Definitions IsNatPowModT, evalNatPowMod	2
Theorems bit0, bit1, run, run', trans, natPow_one_natMod, natPow_zero_natMod_one, natPow_zero_natMod_succ_succ, natPow_zero_natMod_zero	9
Total	11

Mathlib.Meta.NormNum

Definitions

Name	Category	Theorems
IsNatPowModT 📖	CompData	2 math math: IsNatPowModT.bit1, IsNatPowModT.bit0
evalNatPowMod 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natPow_one_natMod 📖	—	—	—	—	natPow_one
natPow_zero_natMod_one 📖	—	—	—	—	pow_zero zero_add
natPow_zero_natMod_succ_succ 📖	—	—	—	—	—
natPow_zero_natMod_zero 📖	—	—	—	—	pow_zero zero_add Nat.modCore.eq_1

Mathlib.Meta.NormNum.IsNatPowModT

Theorems

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

---

← Back to Index