Commit 2025-09-22 11:40 183704f7

View on Github →

feat(Tactic/Ring): handle ℤ-scalar multiplication in the ring tactic (#29782) ring handles ℕ-scalar multiplication; it seems like an accidental omission that it doesn't handle ℤ-scalar multiplication. This PR adds that feature. Everything is directly adapted from the ℕ case. A notable use case for this feature: often abel_nf output contains ℤ-scalar multiplication, so it's important that this can be handled if needed in subsequent ring calls.

Estimated changes

Modified Mathlib/Tactic/Ring/Basic.lean

added def Mathlib.Tactic.Ring.Cache.int

added def Mathlib.Tactic.Ring.evalZSMul

added def Mathlib.Tactic.Ring.instCommSemiringInt

added theorem Mathlib.Tactic.Ring.intCast_add

added theorem Mathlib.Tactic.Ring.intCast_mul

added theorem Mathlib.Tactic.Ring.intCast_negOfNat_Int

added theorem Mathlib.Tactic.Ring.intCast_zero

added theorem Mathlib.Tactic.Ring.natCast_int

added theorem Mathlib.Tactic.Ring.smul_eq_intCast

added theorem Mathlib.Tactic.Ring.smul_int

added def Mathlib.Tactic.Ring.sℤ

added theorem Mathlib.Tactic.Ring.zsmul_congr

Modified Mathlib/Topology/Category/Profinite/Nobeling/Span.lean

Modified MathlibTest/ring.lean