R : Type u_1
inst✝⁵ : Ring R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_2
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
hf : Function.Surjective ↑f
⊢ IsSimpleModule R (M ⧸ ker f)
R : Type u_1
inst✝⁵ : Ring R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_2
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
hf : Function.Surjective ↑f
⊢ IsCoatom (ker f)
rw [← isSimpleModule_iff_isCoatom]
no goals
R : Type u_1
inst✝⁵ : Ring R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_2
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
hf : Function.Surjective ↑f
⊢ IsSimpleModule R (M ⧸ ker f)
exact IsSimpleModule.congr (f.quotKerEquivOfSurjective hf)