Commit 2026-05-24 07:15 f50b40f9

View on Github →

perf: shortcut instances for Semiring (#39719) This PR adds shortcut instances that make sure synthesis using Semiring doesn't go through the other ring-like classes. This matches the new definition of Semiring.

Estimated changes

Modified Mathlib/Algebra/Ring/Defs.lean

Modified Mathlib/Algebra/Ring/Ext.lean

Modified Mathlib/Analysis/Quaternion.lean

added def Quaternion.linearIsometryEquivTuple

added def Quaternion.ofComplex

Modified Mathlib/RingTheory/EuclideanDomain.lean

Modified Mathlib/Tactic/Ring/Basic.lean

modified theorem Mathlib.Tactic.Ring.Int.smul_eq_mul

Modified Mathlib/Topology/Algebra/InfiniteSum/Ring.lean

modified theorem tprod_one_add_ordered

modified theorem tprod_one_sub_ordered

Modified MathlibTest/hintAll.lean