Commit 2025-07-31 17:11 a15945e5

View on Github →

chore: scope or remove some instances (#27592) Per @fpvandoorn's suggestions at #mathlib4 > type-class inference slow/timing out @ 💬.

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/LocallyFiniteOrder.lean

Modified Mathlib/Algebra/Ring/Basic.lean

added theorem Subsingleton.to_noZeroDivisors

Modified Mathlib/GroupTheory/Finiteness.lean

added theorem Monoid.fg_of_finite

Modified Mathlib/LinearAlgebra/FreeModule/Basic.lean

added theorem Module.Free.of_subsingleton'

Modified Mathlib/Order/Disjoint.lean

added theorem Subsingleton.instComplementedLattice

Modified Mathlib/Order/WellQuasiOrder.lean

added theorem Finite.to_wellQuasiOrderedLE

Modified Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean

Modified Mathlib/RingTheory/Artinian/Module.lean

added theorem isArtinian_of_finite