no goals
R : Type u
S : Type v
T : Type w
F : Type ?u.1772041
inst✝¹ : Ring R
inst✝ : Semiring S
rc : RingHomClass F R S
f✝ : F
f : R ≃+* S
⊢ ker ↑f = ⊥
simpa only [← injective_iff_ker_eq_bot] using EquivLike.injective f