R : Type u
S : Type v
F : Type u_1
inst✝¹ : Semiring R
inst✝ : Semiring S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
hK : K ≠ ⊤
⊢ ¬1 ∈ K
R : Type u
S : Type v
F : Type u_1
inst✝¹ : Semiring R
inst✝ : Semiring S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
hK : K ≠ ⊤
⊢ ¬1 ∈ comap f K
rw [mem_comap, map_one]
no goals
R : Type u
S : Type v
F : Type u_1
inst✝¹ : Semiring R
inst✝ : Semiring S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
hK : K ≠ ⊤
⊢ ¬1 ∈ K
exact (ne_top_iff_one _).1 hK