Theorem Basis.constr_range

Modification history

2023-09-21 09:45
Mathlib/LinearAlgebra/Basis.lean
feat: `Hom(N, M)` is Noetherian when `M` is Noetherian and `N` is finitely-generated. (#7276)
Modified Basis.constr_rangeView on Github →
2023-02-28 18:01
Mathlib/LinearAlgebra/Basis.lean
feat: port LinearAlgebra.Basis (#2435)
Added Basis.constr_rangeView on Github →