no goals
R : Type u
S : Type v
T : Type w
F : Type u_1
inst✝¹ : Ring R
inst✝ : Semiring S
rc : RingHomClass F R S
f : F
⊢ ker f = ⊥ ↔ ∀ (x : R), ↑f x = 0 → x = 0
rw [← injective_iff_map_eq_zero f, injective_iff_ker_eq_bot]