Commit 2023-09-21 09:45 63ca289d

View on Github →

feat: Hom(N, M) is Noetherian when M is Noetherian and N is finitely-generated. (#7276)

Estimated changes

Modified Mathlib/Algebra/Module/LinearMap.lean

added theorem Function.Injective.injective_linearMapComp_left

added theorem Function.Surjective.injective_linearMapComp_right

modified theorem LinearMap.cancel_left

modified theorem LinearMap.cancel_right

Modified Mathlib/LinearAlgebra/Basis.lean

modified theorem Basis.constr_range

Modified Mathlib/LinearAlgebra/BilinearMap.lean

Modified Mathlib/LinearAlgebra/Finsupp.lean

modified theorem Finsupp.lmapDomain_supported

Modified Mathlib/LinearAlgebra/StdBasis.lean

added theorem Module.piEquiv_apply_apply

added theorem Module.range_piEquiv

added theorem Module.surjective_piEquiv_apply_iff

Modified Mathlib/RingTheory/Finiteness.lean

added theorem Module.Finite.exists_fin'

Modified Mathlib/RingTheory/Noetherian.lean