Subgroups generated by an element

Tags

subgroup, subgroups

ink

def Subgroup.zpowers {G : Type u_1} [inst : Group G] (g : G) : Subgroup G

The subgroup generated by an element.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Subgroup.mem_zpowers {G : Type u_1} [inst : Group G] (g : G) : g ∈ Subgroup.zpowers g

ink

theorem Subgroup.zpowers_eq_closure {G : Type u_1} [inst : Group G] (g : G) : Subgroup.zpowers g = Subgroup.closure {g}

ink

@[simp]

theorem Subgroup.range_zpowersHom {G : Type u_1} [inst : Group G] (g : G) : MonoidHom.range (↑(zpowersHom G) g) = Subgroup.zpowers g

ink

theorem Subgroup.zpowers_subset {G : Type u_1} [inst : Group G] {a : G} {K : Subgroup G} (h : a ∈ K) : Subgroup.zpowers a ≤ K

ink

theorem Subgroup.mem_zpowers_iff {G : Type u_1} [inst : Group G] {g : G} {h : G} : h ∈ Subgroup.zpowers g ↔ ∃ k, g ^ k = h

ink

@[simp]

theorem Subgroup.zpow_mem_zpowers {G : Type u_1} [inst : Group G] (g : G) (k : ℤ) : g ^ k ∈ Subgroup.zpowers g

ink

@[simp]

theorem Subgroup.npow_mem_zpowers {G : Type u_1} [inst : Group G] (g : G) (k : ℕ) : g ^ k ∈ Subgroup.zpowers g

ink

@[simp]

theorem Subgroup.forall_zpowers {G : Type u_1} [inst : Group G] {x : G} {p : { x // x ∈ Subgroup.zpowers x } → Prop} : ((g : { x // x ∈ Subgroup.zpowers x }) → p g) ↔ (m : ℤ) → p { val := x ^ m, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) x y = x ^ m) }

ink

@[simp]

theorem Subgroup.exists_zpowers {G : Type u_1} [inst : Group G] {x : G} {p : { x // x ∈ Subgroup.zpowers x } → Prop} : (∃ g, p g) ↔ ∃ m, p { val := x ^ m, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) x y = x ^ m) }

ink

theorem Subgroup.forall_mem_zpowers {G : Type u_1} [inst : Group G] {x : G} {p : G → Prop} : ((g : G) → g ∈ Subgroup.zpowers x → p g) ↔ (m : ℤ) → p (x ^ m)

ink

theorem Subgroup.exists_mem_zpowers {G : Type u_1} [inst : Group G] {x : G} {p : G → Prop} : (∃ g, g ∈ Subgroup.zpowers x ∧ p g) ↔ ∃ m, p (x ^ m)

ink

instance Subgroup.instCountableSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupZpowers {G : Type u_1} [inst : Group G] (a : G) : Countable { x // x ∈ Subgroup.zpowers a }

Equations

• @Subgroup.instCountableSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupZpowers = @Subgroup.instCountableSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupZpowers.proof_1

ink

def AddSubgroup.zmultiples {A : Type u_1} [inst : AddGroup A] (a : A) : AddSubgroup A

The subgroup generated by an element.

Equations

• AddSubgroup.zmultiples a = AddSubgroup.copy (AddMonoidHom.range (↑(zmultiplesHom A) a)) (Set.range fun x => x • a) (_ : (Set.range fun x => x • a) = Set.range fun x => x • a)

ink

@[simp]

theorem AddSubgroup.range_zmultiplesHom {A : Type u_1} [inst : AddGroup A] (a : A) : AddMonoidHom.range (↑(zmultiplesHom A) a) = AddSubgroup.zmultiples a

ink

@[simp]

theorem AddSubgroup.mem_zmultiples {G : Type u_1} [inst : AddGroup G] (g : G) : g ∈ AddSubgroup.zmultiples g

ink

theorem AddSubgroup.zmultiples_eq_closure {G : Type u_1} [inst : AddGroup G] (g : G) : AddSubgroup.zmultiples g = AddSubgroup.closure {g}

ink

abbrev AddSubgroup.zmultiples_subset.match_1 {G : Type u_1} [inst : AddGroup G] {a : G} (motive : (x : G) → x ∈ AddSubgroup.zmultiples a → Prop) : (x : G) → (hx : x ∈ AddSubgroup.zmultiples a) → ((i : ℤ) → motive ((fun x x_1 => x_1 • x) a i) (_ : ∃ y, (fun x x_1 => x_1 • x) a y = (fun x x_1 => x_1 • x) a i)) → motive x hx

Equations

• One or more equations did not get rendered due to their size.

ink

theorem AddSubgroup.zmultiples_subset {G : Type u_1} [inst : AddGroup G] {a : G} {K : AddSubgroup G} (h : a ∈ K) : AddSubgroup.zmultiples a ≤ K

ink

theorem AddSubgroup.mem_zmultiples_iff {G : Type u_1} [inst : AddGroup G] {g : G} {h : G} : h ∈ AddSubgroup.zmultiples g ↔ ∃ k, k • g = h

ink

@[simp]

theorem AddSubgroup.zsmul_mem_zmultiples {G : Type u_1} [inst : AddGroup G] (g : G) (k : ℤ) : k • g ∈ AddSubgroup.zmultiples g

ink

@[simp]

theorem AddSubgroup.nsmul_mem_zmultiples {G : Type u_1} [inst : AddGroup G] (g : G) (k : ℕ) : k • g ∈ AddSubgroup.zmultiples g

ink

@[simp]

theorem AddSubgroup.forall_zmultiples {G : Type u_1} [inst : AddGroup G] {x : G} {p : { x // x ∈ AddSubgroup.zmultiples x } → Prop} : ((g : { x // x ∈ AddSubgroup.zmultiples x }) → p g) ↔ (m : ℤ) → p { val := m • x, property := (_ : ∃ y, (fun x x_1 => x_1 • x) x y = m • x) }

ink

theorem AddSubgroup.forall_mem_zmultiples {G : Type u_1} [inst : AddGroup G] {x : G} {p : G → Prop} : ((g : G) → g ∈ AddSubgroup.zmultiples x → p g) ↔ (m : ℤ) → p (m • x)

ink

@[simp]

theorem AddSubgroup.exists_zmultiples {G : Type u_1} [inst : AddGroup G] {x : G} {p : { x // x ∈ AddSubgroup.zmultiples x } → Prop} : (∃ g, p g) ↔ ∃ m, p { val := m • x, property := (_ : ∃ y, (fun x x_1 => x_1 • x) x y = m • x) }

ink

theorem AddSubgroup.exists_mem_zmultiples {G : Type u_1} [inst : AddGroup G] {x : G} {p : G → Prop} : (∃ g, g ∈ AddSubgroup.zmultiples x ∧ p g) ↔ ∃ m, p (m • x)

ink

instance AddSubgroup.instCountableSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupZmultiples {A : Type u_1} [inst : AddGroup A] (a : A) : Countable { x // x ∈ AddSubgroup.zmultiples a }

Equations

• @AddSubgroup.instCountableSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupZmultiples = @AddSubgroup.instCountableSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupZmultiples.proof_1

ink

@[simp]

theorem AddSubgroup.int_cast_mul_mem_zmultiples {R : Type u_1} [inst : Ring R] (r : R) (k : ℤ) : ↑k * r ∈ AddSubgroup.zmultiples r

ink

@[simp]

theorem AddSubgroup.int_cast_mem_zmultiples_one {R : Type u_1} [inst : Ring R] (k : ℤ) : ↑k ∈ AddSubgroup.zmultiples 1

ink

@[simp]

theorem AddMonoidHom.map_zmultiples {G : Type u_1} [inst : AddGroup G] {N : Type u_2} [inst : AddGroup N] (f : G →+ N) (x : G) : AddSubgroup.map f (AddSubgroup.zmultiples x) = AddSubgroup.zmultiples (↑f x)

ink

@[simp]

theorem MonoidHom.map_zpowers {G : Type u_1} [inst : Group G] {N : Type u_2} [inst : Group N] (f : G →* N) (x : G) : Subgroup.map f (Subgroup.zpowers x) = Subgroup.zpowers (↑f x)

ink

theorem Int.mem_zmultiples_iff {a : ℤ} {b : ℤ} : b ∈ AddSubgroup.zmultiples a ↔ a ∣ b

ink

theorem ofMul_image_zpowers_eq_zmultiples_ofMul {G : Type u_1} [inst : Group G] {x : G} : ↑Additive.ofMul '' ↑(Subgroup.zpowers x) = ↑(AddSubgroup.zmultiples (↑Additive.ofMul x))

ink

theorem ofAdd_image_zmultiples_eq_zpowers_ofAdd {A : Type u_1} [inst : AddGroup A] {x : A} : ↑Multiplicative.ofAdd '' ↑(AddSubgroup.zmultiples x) = ↑(Subgroup.zpowers (↑Multiplicative.ofAdd x))

ink

def AddSubgroup.zmultiples_isCommutative.proof_1 {G : Type u_1} [inst : AddGroup G] (g : G) : AddSubgroup.IsCommutative (AddSubgroup.zmultiples g)

Equations

• (_ : AddSubgroup.IsCommutative (AddSubgroup.zmultiples g)) = (_ : AddSubgroup.IsCommutative (AddSubgroup.zmultiples g))

ink

abbrev AddSubgroup.zmultiples_isCommutative.match_1 {G : Type u_1} [inst : AddGroup G] (g : G) (motive : { x // x ∈ AddSubgroup.zmultiples g } → Prop) : (x : { x // x ∈ AddSubgroup.zmultiples g }) → ((val : G) → (w : ℤ) → (h₂ : (fun x x_1 => x_1 • x) g w = val) → motive { val := val, property := (_ : ∃ y, (fun x x_1 => x_1 • x) g y = val) }) → motive x

Equations

• AddSubgroup.zmultiples_isCommutative.match_1 g motive x h_1 = Subtype.casesOn x fun val property => Exists.casesOn property fun w h => h_1 val w h

ink

instance AddSubgroup.zmultiples_isCommutative {G : Type u_1} [inst : AddGroup G] (g : G) : AddSubgroup.IsCommutative (AddSubgroup.zmultiples g)

Equations

• @AddSubgroup.zmultiples_isCommutative = @AddSubgroup.zmultiples_isCommutative.proof_1

ink

instance Subgroup.zpowers_isCommutative {G : Type u_1} [inst : Group G] (g : G) : Subgroup.IsCommutative (Subgroup.zpowers g)

Equations

• @Subgroup.zpowers_isCommutative = @Subgroup.zpowers_isCommutative.proof_1

ink

@[simp]

theorem AddSubgroup.zmultiples_le {G : Type u_1} [inst : AddGroup G] {g : G} {H : AddSubgroup G} : AddSubgroup.zmultiples g ≤ H ↔ g ∈ H

ink

@[simp]

theorem Subgroup.zpowers_le {G : Type u_1} [inst : Group G] {g : G} {H : Subgroup G} : Subgroup.zpowers g ≤ H ↔ g ∈ H

ink

@[simp]

theorem AddSubgroup.zmultiples_eq_bot {G : Type u_1} [inst : AddGroup G] {g : G} : AddSubgroup.zmultiples g = ⊥ ↔ g = 0

ink

@[simp]

theorem Subgroup.zpowers_eq_bot {G : Type u_1} [inst : Group G] {g : G} : Subgroup.zpowers g = ⊥ ↔ g = 1

ink

@[simp]

theorem AddSubgroup.zmultiples_zero_eq_bot {G : Type u_1} [inst : AddGroup G] : AddSubgroup.zmultiples 0 = ⊥

ink

@[simp]

theorem Subgroup.zpowers_one_eq_bot {G : Type u_1} [inst : Group G] : Subgroup.zpowers 1 = ⊥

ink

theorem AddSubgroup.centralizer_closure {G : Type u_1} [inst : AddGroup G] (S : Set G) : AddSubgroup.centralizer (AddSubgroup.closure S) = ⨅ g, ⨅ h, AddSubgroup.centralizer (AddSubgroup.zmultiples g)

ink

theorem Subgroup.centralizer_closure {G : Type u_1} [inst : Group G] (S : Set G) : Subgroup.centralizer (Subgroup.closure S) = ⨅ g, ⨅ h, Subgroup.centralizer (Subgroup.zpowers g)

ink

theorem AddSubgroup.center_eq_infᵢ {G : Type u_1} [inst : AddGroup G] (S : Set G) (hS : AddSubgroup.closure S = ⊤) : AddSubgroup.center G = ⨅ g, ⨅ h, AddSubgroup.centralizer (AddSubgroup.zmultiples g)

ink

theorem Subgroup.center_eq_infᵢ {G : Type u_1} [inst : Group G] (S : Set G) (hS : Subgroup.closure S = ⊤) : Subgroup.center G = ⨅ g, ⨅ h, Subgroup.centralizer (Subgroup.zpowers g)

ink

theorem AddSubgroup.center_eq_infi' {G : Type u_1} [inst : AddGroup G] (S : Set G) (hS : AddSubgroup.closure S = ⊤) : AddSubgroup.center G = ⨅ g, AddSubgroup.centralizer (AddSubgroup.zmultiples ↑g)

ink

theorem Subgroup.center_eq_infi' {G : Type u_1} [inst : Group G] (S : Set G) (hS : Subgroup.closure S = ⊤) : Subgroup.center G = ⨅ g, Subgroup.centralizer (Subgroup.zpowers ↑g)