mathlib3 documentation

group_theory.subgroup.zpowers

Subgroups generated by an element #

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

Tags #

subgroup, subgroups

source
def subgroup.zpowers {G : Type u_1} [group G] (g : G) :
subgroup G

The subgroup generated by an element.

Equations
Instances for subgroup.zpowers
Instances for ↥subgroup.zpowers
source
@[simp]
theorem subgroup.mem_zpowers {G : Type u_1} [group G] (g : G) :
g ∈ subgroup.zpowers g
source
@[norm_cast]
theorem subgroup.coe_zpowers {G : Type u_1} [group G] (g : G) :
↑(subgroup.zpowers g) = set.range (λ (n : ℤ), g ^ n)
source
theorem subgroup.zpowers_eq_closure {G : Type u_1} [group G] (g : G) :
subgroup.zpowers g = subgroup.closure {g}
source
@[simp]
theorem subgroup.range_zpowers_hom {G : Type u_1} [group G] (g : G) :
(⇑(zpowers_hom G) g).range = subgroup.zpowers g
source
theorem subgroup.mem_zpowers_iff {G : Type u_1} [group G] {g h : G} :
h ∈ subgroup.zpowers g ↔ ∃ (k : ℤ), g ^ k = h
source
@[simp]
theorem subgroup.zpow_mem_zpowers {G : Type u_1} [group G] (g : G) (k : ℤ) :
g ^ k ∈ subgroup.zpowers g
source
@[simp]
theorem subgroup.npow_mem_zpowers {G : Type u_1} [group G] (g : G) (k : ℕ) :
g ^ k ∈ subgroup.zpowers g
source
@[simp]
theorem subgroup.forall_zpowers {G : Type u_1} [group G] {x : G} {p : ↥(subgroup.zpowers x) → Prop} :
(∀ (g : ↥(subgroup.zpowers x)), p g) ↔ ∀ (m : ℤ), p ⟨x ^ m, _⟩
source
@[simp]
theorem subgroup.exists_zpowers {G : Type u_1} [group G] {x : G} {p : ↥(subgroup.zpowers x) → Prop} :
(∃ (g : ↥(subgroup.zpowers x)), p g) ↔ ∃ (m : ℤ), p ⟨x ^ m, _⟩
source
theorem subgroup.forall_mem_zpowers {G : Type u_1} [group G] {x : G} {p : G → Prop} :
(∀ (g : G), g ∈ subgroup.zpowers x → p g) ↔ ∀ (m : ℤ), p (x ^ m)
source
theorem subgroup.exists_mem_zpowers {G : Type u_1} [group G] {x : G} {p : G → Prop} :
(∃ (g : G) (H : g ∈ subgroup.zpowers x), p g) ↔ ∃ (m : ℤ), p (x ^ m)
source
@[protected, instance]
def subgroup.zpowers.countable {G : Type u_1} [group G] (a : G) :
countable ↥(subgroup.zpowers a)
source
def add_subgroup.zmultiples {A : Type u_2} [add_group A] (a : A) :
add_subgroup A

The subgroup generated by an element.

Equations
Instances for add_subgroup.zmultiples
Instances for ↥add_subgroup.zmultiples
source
@[simp]
theorem add_subgroup.range_zmultiples_hom {A : Type u_2} [add_group A] (a : A) :
(⇑(zmultiples_hom A) a).range = add_subgroup.zmultiples a
source
@[simp]
theorem add_subgroup.mem_zmultiples {G : Type u_1} [add_group G] (g : G) :
g ∈ add_subgroup.zmultiples g
source
@[norm_cast]
theorem add_subgroup.coe_zmultiples {G : Type u_1} [add_group G] (g : G) :
↑(add_subgroup.zmultiples g) = set.range (λ (n : ℤ), n • g)
source
theorem add_subgroup.zmultiples_eq_closure {G : Type u_1} [add_group G] (g : G) :
add_subgroup.zmultiples g = add_subgroup.closure {g}
source
theorem add_subgroup.mem_zmultiples_iff {G : Type u_1} [add_group G] {g h : G} :
h ∈ add_subgroup.zmultiples g ↔ ∃ (k : ℤ), k • g = h
source
@[simp]
theorem add_subgroup.zsmul_mem_zmultiples {G : Type u_1} [add_group G] (g : G) (k : ℤ) :
k • g ∈ add_subgroup.zmultiples g
source
@[simp]
theorem add_subgroup.nsmul_mem_zmultiples {G : Type u_1} [add_group G] (g : G) (k : ℕ) :
k • g ∈ add_subgroup.zmultiples g
source
@[simp]
theorem add_subgroup.forall_zmultiples {G : Type u_1} [add_group G] {x : G} {p : ↥(add_subgroup.zmultiples x) → Prop} :
(∀ (g : ↥(add_subgroup.zmultiples x)), p g) ↔ ∀ (m : ℤ), p ⟨m • x, _⟩
source
theorem add_subgroup.forall_mem_zmultiples {G : Type u_1} [add_group G] {x : G} {p : G → Prop} :
(∀ (g : G), g ∈ add_subgroup.zmultiples x → p g) ↔ ∀ (m : ℤ), p (m • x)
source
@[simp]
theorem add_subgroup.exists_zmultiples {G : Type u_1} [add_group G] {x : G} {p : ↥(add_subgroup.zmultiples x) → Prop} :
(∃ (g : ↥(add_subgroup.zmultiples x)), p g) ↔ ∃ (m : ℤ), p ⟨m • x, _⟩
source
theorem add_subgroup.exists_mem_zmultiples {G : Type u_1} [add_group G] {x : G} {p : G → Prop} :
(∃ (g : G) (H : g ∈ add_subgroup.zmultiples x), p g) ↔ ∃ (m : ℤ), p (m • x)
source
@[protected, instance]
def add_subgroup.zmultiples.countable {A : Type u_2} [add_group A] (a : A) :
countable ↥(add_subgroup.zmultiples a)
source
@[simp]
theorem add_subgroup.int_cast_mul_mem_zmultiples {R : Type u_4} [ring R] (r : R) (k : ℤ) :
↑k * r ∈ add_subgroup.zmultiples r
source
@[simp]
theorem add_subgroup.int_cast_mem_zmultiples_one {R : Type u_4} [ring R] (k : ℤ) :
↑k ∈ add_subgroup.zmultiples 1
source
@[simp]
theorem add_monoid_hom.map_zmultiples {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) (x : G) :
add_subgroup.map f (add_subgroup.zmultiples x) = add_subgroup.zmultiples (⇑f x)
source
@[simp]
theorem monoid_hom.map_zpowers {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) (x : G) :
subgroup.map f (subgroup.zpowers x) = subgroup.zpowers (⇑f x)
source
theorem int.mem_zmultiples_iff {a b : ℤ} :
b ∈ add_subgroup.zmultiples a ↔ a ∣ b
source
theorem of_mul_image_zpowers_eq_zmultiples_of_mul {G : Type u_1} [group G] {x : G} :
⇑additive.of_mul '' ↑(subgroup.zpowers x) = ↑(add_subgroup.zmultiples (⇑additive.of_mul x))
source
theorem of_add_image_zmultiples_eq_zpowers_of_add {A : Type u_2} [add_group A] {x : A} :
⇑multiplicative.of_add '' ↑(add_subgroup.zmultiples x) = ↑(subgroup.zpowers (⇑multiplicative.of_add x))
source
@[protected, instance]
def subgroup.zpowers_is_commutative {G : Type u_1} [group G] (g : G) :
(subgroup.zpowers g).is_commutative
source
@[protected, instance]
def add_subgroup.zmultiples_is_commutative {G : Type u_1} [add_group G] (g : G) :
(add_subgroup.zmultiples g).is_commutative
source
@[simp]
theorem subgroup.zpowers_le {G : Type u_1} [group G] {g : G} {H : subgroup G} :
subgroup.zpowers g ≤ H ↔ g ∈ H
source
@[simp]
theorem add_subgroup.zmultiples_le {G : Type u_1} [add_group G] {g : G} {H : add_subgroup G} :
add_subgroup.zmultiples g ≤ H ↔ g ∈ H
source
theorem subgroup.zpowers_le_of_mem {G : Type u_1} [group G] {g : G} {H : subgroup G} :
g ∈ H → subgroup.zpowers g ≤ H

Alias of the reverse direction of subgroup.zpowers_le.

source
theorem add_subgroup.zmultiples_le_of_mem {G : Type u_1} [add_group G] {g : G} {H : add_subgroup G} :
g ∈ H → add_subgroup.zmultiples g ≤ H

Alias of the reverse direction of add_subgroup.zmultiples_le.

source
@[simp]
theorem add_subgroup.zmultiples_eq_bot {G : Type u_1} [add_group G] {g : G} :
add_subgroup.zmultiples g = ⊥ ↔ g = 0
source
@[simp]
theorem subgroup.zpowers_eq_bot {G : Type u_1} [group G] {g : G} :
subgroup.zpowers g = ⊥ ↔ g = 1
source
theorem subgroup.zpowers_ne_bot {G : Type u_1} [group G] {g : G} :
subgroup.zpowers g ≠ ⊥ ↔ g ≠ 1
source
theorem add_subgroup.zmultiples_ne_bot {G : Type u_1} [add_group G] {g : G} :
add_subgroup.zmultiples g ≠ ⊥ ↔ g ≠ 0
source
@[simp]
theorem subgroup.zpowers_one_eq_bot {G : Type u_1} [group G] :
subgroup.zpowers 1 = ⊥
source
@[simp]
theorem add_subgroup.zmultiples_zero_eq_bot {G : Type u_1} [add_group G] :
add_subgroup.zmultiples 0 = ⊥
source
theorem subgroup.centralizer_closure {G : Type u_1} [group G] (S : set G) :
(subgroup.closure S).centralizer = ⨅ (g : G) (H : g ∈ S), (subgroup.zpowers g).centralizer
source
theorem add_subgroup.centralizer_closure {G : Type u_1} [add_group G] (S : set G) :
(add_subgroup.closure S).centralizer = ⨅ (g : G) (H : g ∈ S), (add_subgroup.zmultiples g).centralizer
source
theorem add_subgroup.center_eq_infi {G : Type u_1} [add_group G] (S : set G) (hS : add_subgroup.closure S = ⊤) :
add_subgroup.center G = ⨅ (g : G) (H : g ∈ S), (add_subgroup.zmultiples g).centralizer
source
theorem subgroup.center_eq_infi {G : Type u_1} [group G] (S : set G) (hS : subgroup.closure S = ⊤) :
subgroup.center G = ⨅ (g : G) (H : g ∈ S), (subgroup.zpowers g).centralizer
source
theorem subgroup.center_eq_infi' {G : Type u_1} [group G] (S : set G) (hS : subgroup.closure S = ⊤) :
subgroup.center G = ⨅ (g : ↥S), (subgroup.zpowers ↑g).centralizer
source
theorem add_subgroup.center_eq_infi' {G : Type u_1} [add_group G] (S : set G) (hS : add_subgroup.closure S = ⊤) :
add_subgroup.center G = ⨅ (g : ↥S), (add_subgroup.zmultiples ↑g).centralizer