Theorem Mathlib.Meta.NormNum.natPow_zero_natMod_succ_succ

Modification history

2024-10-23 22:11
Mathlib/Tactic/NormNum/PowMod.lean
feat(Tactic/ReduceModChar): add fast modular exponentiation (#18030) …
Added Mathlib.Meta.NormNum.natPow_zero_natMod_succ_succView on Github →