Theorem Mathlib.Meta.NormNum.IsNatPowModT.bit1

Modification history

2024-10-23 22:11

Mathlib/Tactic/NormNum/PowMod.lean

feat(Tactic/ReduceModChar): add fast modular exponentiation (#18030) …

Added Mathlib.Meta.NormNum.IsNatPowModT.bit1 View on Github →