no goals
R : Type u
S : Type v
T : Type w
F : Type ?u.1774019
inst✝² : Ring R
inst✝¹ : Semiring S
rc : RingHomClass F R S
f✝ : F
F' : Type u_1
inst✝ : RingEquivClass F' R S
f : F'
⊢ ker f = ⊥
simpa only [← injective_iff_ker_eq_bot] using EquivLike.injective f