Theorem LinearMap.FiniteRangeSetoid.equiv_iff_isNoetherian_quotient_eqLocus

Modification history

2026-05-25 15:44
Mathlib/Algebra/Module/LinearMap/FiniteRange.lean
feat: LinearMap.HasFiniteRange and the associated relation (#39468) …
Added LinearMap.FiniteRangeSetoid.equiv_iff_isNoetherian_quotient_eqLocusView on Github →