Commit 2026-04-15 21:15 2be1d772

View on Github →

chore: fix more leaky instances (#38089) Fix some more leaky instances using inferInstanceAs, deriving and fast_instance%

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/DirectSum/Internal.lean

Modified Mathlib/Algebra/Group/Invertible/Basic.lean

Modified Mathlib/Algebra/Group/WithOne/Defs.lean

Modified Mathlib/Algebra/Module/Torsion/Basic.lean

Modified Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

Modified Mathlib/Algebra/Order/Ring/StandardPart.lean

Modified Mathlib/Algebra/Polynomial/Module/Basic.lean

added def PolynomialModule.comp

added def PolynomialModule.equivPolynomial

added def PolynomialModule.equivPolynomialSelf

added def PolynomialModule.eval

added def PolynomialModule.lsingle

added def PolynomialModule.map

added def PolynomialModule.single

Modified Mathlib/Algebra/PresentedMonoid/Basic.lean

modified def PresentedMonoid

Modified Mathlib/Algebra/Quaternion.lean

Modified Mathlib/FieldTheory/RatFunc/Valuation.lean

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

Modified Mathlib/NumberTheory/Cyclotomic/Basic.lean

Modified Mathlib/NumberTheory/NumberField/AdeleRing.lean

Modified Mathlib/RepresentationTheory/Basic.lean