Def Mathlib.Tactic.Ring.sℤ

Modification history

2026-04-06 00:30

Mathlib/Tactic/Ring/Common.lean

refactor(Tactic): change `ring` to allow for coefficients in a variable type (#34734) …

Deleted Mathlib.Tactic.Ring.sℤ View on Github →

2026-02-09 23:46

Mathlib/Tactic/Ring/Common.lean

chore: minimize `meta` imports in `ring`, `abel`, `field_simp` (#34823)

Modified Mathlib.Tactic.Ring.sℤ View on Github →

2026-02-04 23:34

Mathlib/Tactic/Ring/Basic.lean

refactor(Tactic/Ring): move most `ring` code into Common.lean (#34837) …

Modified Mathlib.Tactic.Ring.sℤ View on Github →

2025-09-22 11:40

Mathlib/Tactic/Ring/Basic.lean

feat(Tactic/Ring): handle `ℤ`-scalar multiplication in the ring tactic (#29782) …

Added Mathlib.Tactic.Ring.sℤ View on Github →