R : Type u
S : Type v
T : Type w
F : Type u_1
G : Type ?u.1722384
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : Semiring T
rcf : RingHomClass F R S
rcg : RingHomClass G T S
f✝ : F
g : G
inst✝ : Nontrivial S
f : F
⊢ ¬1 = 0
R : Type u
S : Type v
T : Type w
F : Type u_1
G : Type ?u.1722384
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : Semiring T
rcf : RingHomClass F R S
rcg : RingHomClass G T S
f✝ : F
g : G
inst✝ : Nontrivial S
f : F
⊢ ¬1 ∈ ker f
rw [mem_ker, map_one]
no goals
R : Type u
S : Type v
T : Type w
F : Type u_1
G : Type ?u.1722384
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : Semiring T
rcf : RingHomClass F R S
rcg : RingHomClass G T S
f✝ : F
g : G
inst✝ : Nontrivial S
f : F
⊢ ¬1 = 0
exact one_ne_zero