Commit 2026-05-25 15:44 b002f16e

feat: LinearMap.HasFiniteRange and the associated relation (#39468) We add two predicates on linear maps: HasFiniteRange says that the range is finitely generated, and HasNoetherianRange says that the range is noetherian. We also add the equivalence relation on linear maps saying that two maps differ by a linear map with noetherian range, and prove that it's compatible with addition and composition. This was originally written by @PatrickMassot at the May 2026 ICERM workshop as part of the project on Fredholm operators. This also adds four supporting lemmas: map_smul_le_map, range_smul_le_range, ker_le_ker_smul and isNoetherian_map.