no goals
R : Type u_1
R₂ : Type u_4
K : Type ?u.307925
M : Type u_2
M₂ : Type u_3
V : Type ?u.307934
S : Type ?u.307937
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
p p' : Submodule R M
⊢ map f p ≤ map f p' ↔ p ≤ p' ⊔ ker f
rw [map_le_iff_le_comap, Submodule.comap_map_eq]