theorem
AddSubgroup.ker_saturated
{A₁ : Type u_1}
{A₂ : Type u_2}
[AddCommGroup A₁]
[AddCommGroup A₂]
[NoZeroSMulDivisors ℕ A₂]
(f : A₁ →+ A₂)
:

f.ker.Saturated

theorem
AddSubgroup.ker_saturated
{A₁ : Type u_1}
{A₂ : Type u_2}
[AddCommGroup A₁]
[AddCommGroup A₂]
[NoZeroSMulDivisors ℕ A₂]
(f : A₁ →+ A₂)
:

f.ker.Saturated