Commit 2025-08-16 00:34 f07e974e

View on Github →

feat: make ring work for semifields (#28494) Generalize ring's division ring theorems to division semiring. This means ring will work for commutative division semirings aka semifields. From #mathlib4 > ring for NNReal @ 💬

Estimated changes

Modified Mathlib/Tactic/Ring/Basic.lean

modified def Mathlib.Tactic.Ring.Cache.nat

modified theorem Mathlib.Tactic.Ring.div_congr

modified theorem Mathlib.Tactic.Ring.div_pf

modified def Mathlib.Tactic.Ring.evalDiv

modified theorem Mathlib.Tactic.Ring.inv_congr

modified theorem Mathlib.Tactic.Ring.inv_mul

modified theorem Mathlib.Tactic.Ring.inv_single

Modified MathlibTest/ring.lean