An additive subgroup `H`

of `G`

is *saturated* if for all `n : ℕ`

and `g : G`

with `n•g ∈ H`

we have `n = 0`

or `g ∈ H`

.

## Instances For

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