R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
h : I ≤ J
⊢ I ≤ J
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
h : I ≤ J
⊢ map (Quotient.mk J) I = ⊥
rw [map_eq_bot_iff_le_ker, mk_ker]
no goals
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
h : I ≤ J
⊢ I ≤ J
exact h