Commit 2026-06-04 12:28 f5bbbdfe

View on Github →

perf: another shortcut instance for Semiring (#40153) This PR adds another shortcut instance for Semiring that I had missed in #39719, because I assumed that it had already been tagged as an instance automatically.

Estimated changes

Modified Mathlib/Algebra/Ring/Defs.lean

Modified Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean

Modified Mathlib/FieldTheory/PurelyInseparable/Tower.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

modified theorem QuadraticMap.associated_sq

Modified Mathlib/NumberTheory/TsumDivisorsAntidiagonal.lean

Modified Mathlib/RingTheory/HahnSeries/Cardinal.lean

Modified Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean

Modified Mathlib/RingTheory/QuasiFinite/Basic.lean