Commit 2024-10-23 22:11 b65e87ab

View on Github →

feat(Tactic/ReduceModChar): add fast modular exponentiation (#18030) This PR (done by Markus Himmel, with minor clean-up from Quang Dao) introduces fast modular exponentiation to the reduce_mod_char tactic. This allows for exponentiating large number reduced modulo n for some n. An example is:

example : (-126432 : ZMod 1235412223) ^ 12355342321 = 1001528716 := by reduce_mod_char

See the new tests for more examples.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/NumberTheory/LucasPrimality.lean

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/NormNum/Core.lean

Created Mathlib/Tactic/NormNum/PowMod.lean

added theorem Mathlib.Meta.NormNum.IsNatPowModT.bit0

added theorem Mathlib.Meta.NormNum.IsNatPowModT.bit1

added theorem Mathlib.Meta.NormNum.IsNatPowModT.run

added theorem Mathlib.Meta.NormNum.IsNatPowModT.trans

added structure Mathlib.Meta.NormNum.IsNatPowModT

added theorem Mathlib.Meta.NormNum.natPow_one_natMod

added theorem Mathlib.Meta.NormNum.natPow_zero_natMod_one

added theorem Mathlib.Meta.NormNum.natPow_zero_natMod_succ_succ

added theorem Mathlib.Meta.NormNum.natPow_zero_natMod_zero

Modified Mathlib/Tactic/ReduceModChar.lean

modified theorem Tactic.ReduceModChar.CharP.isInt_of_mod

added theorem Tactic.ReduceModChar.CharP.isNat_pow

added def Tactic.ReduceModChar.normBareNumeral

Modified test/norm_num_ext.lean

Modified test/reduce_mod_char.lean

added def q'