exact ⟨a, Subtype.val_injective ha⟩
case hN.intro
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
N : Submodule R M
M' : Type u_1
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
l : M →ₗ[R] M'
inst✝ : Module.Finite R ↥N
hN : N ⊓ LinearMap.ker l ≤ Submodule.torsion R M
x : ↥N
hx : x ∈ LinearMap.ker (l ∘ₗ N.subtype)
a : ↥(nonZeroDivisors R)
ha : a • ↑x = 0
⊢ x ∈ Submodule.torsion R ↥N
no goals