no goals
R : Type u
S : Type v
T : Type w
F : Type u_1
G : Type ?u.1679598
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
rcf : RingHomClass F R S
rcg : RingHomClass G T S
f : F
g : G
r : R
⊢ r ∈ ker f ↔ ↑f r = 0
rw [ker, Ideal.mem_comap, Submodule.mem_bot]