Commit 2026-02-09 23:46 97d681bb

View on Github →

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

Estimated changes

Modified Mathlib/Tactic/Abel.lean

Modified Mathlib/Tactic/Attr/Register.lean

Modified Mathlib/Tactic/FieldSimp.lean

modified def Mathlib.Tactic.FieldSimp.qNF.toNF

Modified Mathlib/Tactic/FieldSimp/Lemmas.lean

Modified Mathlib/Tactic/Hint.lean

Modified Mathlib/Tactic/NormNum/Basic.lean

Modified Mathlib/Tactic/NormNum/Core.lean

Modified Mathlib/Tactic/NormNum/Result.lean

Modified Mathlib/Tactic/Positivity/Core.lean

Modified Mathlib/Tactic/Ring.lean

Modified Mathlib/Tactic/Ring/Basic.lean

Modified Mathlib/Tactic/Ring/Common.lean

deleted inductive Mathlib.Tactic.Ring.ExBase

deleted inductive Mathlib.Tactic.Ring.ExProd

deleted inductive Mathlib.Tactic.Ring.ExSum

deleted def Mathlib.Tactic.Ring.instCommSemiringInt

deleted def Mathlib.Tactic.Ring.instCommSemiringNat

modified def Mathlib.Tactic.Ring.sℕ

modified def Mathlib.Tactic.Ring.sℤ

Modified Mathlib/Tactic/Ring/RingNF.lean

Modified Mathlib/Util/DischargerAsTactic.lean

Modified Mathlib/Util/Qq.lean