Module.Finite.of_ker_le_range_of_isNoetherianRing
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Finite_of_ker_le_range_of_isNoetherianRingLean source · statement
theorem _root_.Module.Finite.of_ker_le_range_of_isNoetherianRing {R : Type*} [CommRing R]
[IsNoetherianRing R] {M N₁ N₂ : Type*} [AddCommGroup M] [Module R M]
[AddCommGroup N₁] [Module R N₁] [AddCommGroup N₂] [Module R N₂] [Module.Finite R N₁]
[Module.Finite R N₂]
(α : N₁ →ₗ[R] M) (β : M →ₗ[R] N₂) (h : LinearMap.ker β ≤ LinearMap.range α) : Module.Finite
R M