R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type ?u.14646
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ IsSimpleModule R { x // x ∈ m } ↔ IsSimpleOrder ↑(Set.Iic m)
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type ?u.14646
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ IsSimpleModule R { x // x ∈ m } ↔ IsAtom m
rw [← Set.isSimpleOrder_Iic_iff_isAtom]
case f
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type ?u.14646
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ Submodule R { x // x ∈ m } ≃o ↑(Set.Iic m)
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type ?u.14646
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ IsSimpleModule R { x // x ∈ m } ↔ IsSimpleOrder ↑(Set.Iic m)
apply OrderIso.isSimpleOrder_iff
no goals
case f
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type ?u.14646
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ Submodule R { x // x ∈ m } ≃o ↑(Set.Iic m)
exact Submodule.MapSubtype.relIso m