LeanPool.BrauerGroupNew.Mathlib.RingTheory.TwoSidedIdeal.Kernel #
Imported Lean Pool material for LeanPool.BrauerGroupNew.Mathlib.RingTheory.TwoSidedIdeal.Kernel.
theorem
TwoSidedIdeal.injective_iff_ker_eq_bot
{R : Type u_1}
{S : Type u_2}
[Ring R]
[Ring S]
{F : Type u_3}
[FunLike F R S]
[RingHomClass F R S]
(f : F)
: