case intro.intro
R : Type u_1
M : Type u_2
P : Type ?u.268814
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
s : Surjective ↑f
n : ℕ
ne : n ≠ 0
w : LinearMap.ker (f ^ n) ⊓ LinearMap.range (f ^ n) = ⊥
⊢ Injective ↑f
R : Type u_1
M : Type u_2
P : Type ?u.268814
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
s : Surjective ↑f
⊢ Injective ↑f
obtain ⟨n, ne, w⟩ := IsNoetherian.exists_endomorphism_iterate_ker_inf_range_eq_bot f
case intro.intro
R : Type u_1
M : Type u_2
P : Type ?u.268814
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
s : Surjective ↑f
n : ℕ
ne : n ≠ 0
w : Injective ↑(f ^ n)
⊢ Injective ↑f
case intro.intro
R : Type u_1
M : Type u_2
P : Type ?u.268814
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
s : Surjective ↑f
n : ℕ
ne : n ≠ 0
w : LinearMap.ker (f ^ n) ⊓ LinearMap.range (f ^ n) = ⊥
⊢ Injective ↑f
rw [LinearMap.range_eq_top.mpr (LinearMap.iterate_surjective s n), inf_top_eq,
  LinearMap.ker_eq_bot] at w
no goals
case intro.intro
R : Type u_1
M : Type u_2
P : Type ?u.268814
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
s : Surjective ↑f
n : ℕ
ne : n ≠ 0
w : Injective ↑(f ^ n)
⊢ Injective ↑f
exact LinearMap.injective_of_iterate_injective ne w