Theorem Tactic.ReduceModChar.CharP.isNat_pow

Modification history

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