Commit 2023-11-09 13:54 928e39cc

feat: reduce_mod_char tactic for reducing numeric expressions in positive characteristic (#5376) This PR defines the reduce_mod_char tactic, which traverses expressions looking for numerals n, such that the type of n is a ring of (positive) characteristic p, and reduces these numerals modulo p, to lie between 0 and p. This is one of my first Lean 4 metaprogramming projects, so I eagerly await you pointing out all my mistakes. Especially I would like to learn where I should insert those magical withContext and instantiateMVars incantations. Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/tactic.20for.20easy.20calculations.20in.20ZMod.20p.3F