Saturated subgroups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Tags #

subgroup, subgroups

def add_subgroup.saturated {G : Type u_1} [add_group G] (H : add_subgroup G) :

Prop

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.

Equations

def subgroup.saturated {G : Type u_1} [group G] (H : subgroup G) :

Prop

A subgroup H of G is saturated if for all n : ℕ and g : G with g^n ∈ H we have n = 0 or g ∈ H.

Equations

theorem subgroup.saturated_iff_npow {G : Type u_1} [group G] {H : subgroup G} :

H.saturated ↔ ∀ (n : ℕ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H

theorem add_subgroup.saturated_iff_nsmul {G : Type u_1} [add_group G] {H : add_subgroup G} :

H.saturated ↔ ∀ (n : ℕ) (g : G), n • g ∈ H → n = 0 ∨ g ∈ H

theorem add_subgroup.saturated_iff_zsmul {G : Type u_1} [add_group G] {H : add_subgroup G} :

H.saturated ↔ ∀ (n : ℤ) (g : G), n • g ∈ H → n = 0 ∨ g ∈ H

theorem subgroup.saturated_iff_zpow {G : Type u_1} [group G] {H : subgroup G} :

H.saturated ↔ ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H

theorem add_subgroup.ker_saturated {A₁ : Type u_1} {A₂ : Type u_2} [add_comm_group A₁] [add_comm_group A₂] [no_zero_smul_divisors ℕ A₂] (f : A₁ →+ A₂) :