Documentation

Mathlib.Algebra.Group.Subgroup.ZPowers

Subgroups generated by an element #

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
source
@[simp]
theorem Subgroup.mem_zpowers {G : Type u_1} [Group G] (g : G) :
g ∈ Subgroup.zpowers g
source
theorem Subgroup.coe_zpowers {G : Type u_1} [Group G] (g : G) :
↑(Subgroup.zpowers g) = Set.range fun (x : ℤ) => g ^ x
source
noncomputable instance Subgroup.decidableMemZPowers {G : Type u_1} [Group G] {a : G} :
DecidablePred fun (x : G) => x ∈ Subgroup.zpowers a
Equations
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_zpowersHom {G : Type u_1} [Group G] (g : G) :
((zpowersHom G) g).range = Subgroup.zpowers g
source
theorem Subgroup.mem_zpowers_iff {G : Type u_1} [Group G] {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 : { x_1 : G // x_1 ∈ Subgroup.zpowers x } → Prop} :
(∀ (g : { x_1 : G // x_1 ∈ Subgroup.zpowers x }), p g) ↔ ∀ (m : ℤ), p ⟨x ^ m, ⋯⟩
source
@[simp]
theorem Subgroup.exists_zpowers {G : Type u_1} [Group G] {x : G} {p : { x_1 : G // x_1 ∈ Subgroup.zpowers x } → Prop} :
(∃ (g : { x_1 : G // x_1 ∈ 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 ∈ 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 ∈ Subgroup.zpowers x, p g) ↔ ∃ (m : ℤ), p (x ^ m)
source
instance Subgroup.instCountableSubtypeMemZpowers {G : Type u_1} [Group G] (a : G) :
Countable { x : G // x ∈ Subgroup.zpowers a }
Equations
  • ⋯ = ⋯
source
def AddSubgroup.zmultiples {A : Type u_2} [AddGroup A] (a : A) :
AddSubgroup A

The subgroup generated by an element.

Equations
Instances For
source
@[simp]
theorem AddSubgroup.range_zmultiplesHom {A : Type u_2} [AddGroup A] (a : A) :
((zmultiplesHom A) a).range = AddSubgroup.zmultiples a
source
@[simp]
theorem AddSubgroup.mem_zmultiples {G : Type u_1} [AddGroup G] (g : G) :
g ∈ AddSubgroup.zmultiples g
source
theorem AddSubgroup.coe_zmultiples {G : Type u_1} [AddGroup G] (g : G) :
↑(AddSubgroup.zmultiples g) = Set.range fun (x : ℤ) => x • g
source
noncomputable instance AddSubgroup.decidableMemZMultiples {G : Type u_1} [AddGroup G] {a : G} :
DecidablePred fun (x : G) => x ∈ AddSubgroup.zmultiples a
Equations
source
theorem AddSubgroup.zmultiples_eq_closure {G : Type u_1} [AddGroup G] (g : G) :
AddSubgroup.zmultiples g = AddSubgroup.closure {g}
source
theorem AddSubgroup.mem_zmultiples_iff {G : Type u_1} [AddGroup G] {g : G} {h : G} :
h ∈ AddSubgroup.zmultiples g ↔ ∃ (k : ℤ), k • g = h
source
@[simp]
theorem AddSubgroup.zsmul_mem_zmultiples {G : Type u_1} [AddGroup G] (g : G) (k : ℤ) :
k • g ∈ AddSubgroup.zmultiples g
source
@[simp]
theorem AddSubgroup.nsmul_mem_zmultiples {G : Type u_1} [AddGroup G] (g : G) (k : ℕ) :
k • g ∈ AddSubgroup.zmultiples g
source
@[simp]
theorem AddSubgroup.forall_zmultiples {G : Type u_1} [AddGroup G] {x : G} {p : { x_1 : G // x_1 ∈ AddSubgroup.zmultiples x } → Prop} :
(∀ (g : { x_1 : G // x_1 ∈ AddSubgroup.zmultiples x }), p g) ↔ ∀ (m : ℤ), p ⟨m • x, ⋯⟩
source
theorem AddSubgroup.forall_mem_zmultiples {G : Type u_1} [AddGroup G] {x : G} {p : G → Prop} :
(∀ g ∈ AddSubgroup.zmultiples x, p g) ↔ ∀ (m : ℤ), p (m • x)
source
@[simp]
theorem AddSubgroup.exists_zmultiples {G : Type u_1} [AddGroup G] {x : G} {p : { x_1 : G // x_1 ∈ AddSubgroup.zmultiples x } → Prop} :
(∃ (g : { x_1 : G // x_1 ∈ AddSubgroup.zmultiples x }), p g) ↔ ∃ (m : ℤ), p ⟨m • x, ⋯⟩
source
theorem AddSubgroup.exists_mem_zmultiples {G : Type u_1} [AddGroup G] {x : G} {p : G → Prop} :
(∃ g ∈ AddSubgroup.zmultiples x, p g) ↔ ∃ (m : ℤ), p (m • x)
source
instance AddSubgroup.instCountableSubtypeMemZmultiples {A : Type u_2} [AddGroup A] (a : A) :
Countable { x : A // x ∈ AddSubgroup.zmultiples a }
Equations
  • ⋯ = ⋯
source
@[simp]
theorem AddSubgroup.intCast_mul_mem_zmultiples {R : Type u_4} [Ring R] (r : R) (k : ℤ) :
↑k * r ∈ AddSubgroup.zmultiples r
source
@[deprecated AddSubgroup.intCast_mul_mem_zmultiples]
theorem AddSubgroup.int_cast_mul_mem_zmultiples {R : Type u_4} [Ring R] (r : R) (k : ℤ) :
↑k * r ∈ AddSubgroup.zmultiples r

Alias of AddSubgroup.intCast_mul_mem_zmultiples.

source
@[simp]
theorem AddSubgroup.intCast_mem_zmultiples_one {R : Type u_4} [Ring R] (k : ℤ) :
↑k ∈ AddSubgroup.zmultiples 1
source
@[deprecated AddSubgroup.intCast_mem_zmultiples_one]
theorem AddSubgroup.int_cast_mem_zmultiples_one {R : Type u_4} [Ring R] (k : ℤ) :
↑k ∈ AddSubgroup.zmultiples 1

Alias of AddSubgroup.intCast_mem_zmultiples_one.

source
@[simp]
theorem Int.range_castAddHom {A : Type u_4} [AddGroupWithOne A] :
(Int.castAddHom A).range = AddSubgroup.zmultiples 1
source
@[simp]
theorem AddMonoidHom.map_zmultiples {G : Type u_1} [AddGroup G] {N : Type u_3} [AddGroup N] (f : G →+ N) (x : G) :
AddSubgroup.map f (AddSubgroup.zmultiples x) = AddSubgroup.zmultiples (f x)
source
@[simp]
theorem MonoidHom.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 ∈ AddSubgroup.zmultiples a ↔ a ∣ b
source
@[simp]
theorem Int.zmultiples_one :
AddSubgroup.zmultiples 1 = ⊤
source
theorem ofMul_image_zpowers_eq_zmultiples_ofMul {G : Type u_1} [Group G] {x : G} :
⇑Additive.ofMul '' ↑(Subgroup.zpowers x) = ↑(AddSubgroup.zmultiples (Additive.ofMul x))
source
theorem ofAdd_image_zmultiples_eq_zpowers_ofAdd {A : Type u_2} [AddGroup A] {x : A} :
⇑Multiplicative.ofAdd '' ↑(AddSubgroup.zmultiples x) = ↑(Subgroup.zpowers (Multiplicative.ofAdd x))
source
instance AddSubgroup.zmultiples_isCommutative {G : Type u_1} [AddGroup G] (g : G) :
(AddSubgroup.zmultiples g).IsCommutative
Equations
  • ⋯ = ⋯
source
instance Subgroup.zpowers_isCommutative {G : Type u_1} [Group G] (g : G) :
(Subgroup.zpowers g).IsCommutative
Equations
  • ⋯ = ⋯
source
@[simp]
theorem AddSubgroup.zmultiples_le {G : Type u_1} [AddGroup G] {g : G} {H : AddSubgroup G} :
AddSubgroup.zmultiples g ≤ H ↔ g ∈ H
source
@[simp]
theorem Subgroup.zpowers_le {G : Type u_1} [Group G] {g : G} {H : Subgroup G} :
Subgroup.zpowers 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 AddSubgroup.zmultiples_le_of_mem {G : Type u_1} [AddGroup G] {g : G} {H : AddSubgroup G} :
g ∈ H → AddSubgroup.zmultiples g ≤ H

Alias of the reverse direction of AddSubgroup.zmultiples_le.

source
@[simp]
theorem AddSubgroup.zmultiples_eq_bot {G : Type u_1} [AddGroup G] {g : G} :
AddSubgroup.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 AddSubgroup.zmultiples_ne_bot {G : Type u_1} [AddGroup G] {g : G} :
AddSubgroup.zmultiples g ≠ ⊥ ↔ g ≠ 0
source
theorem Subgroup.zpowers_ne_bot {G : Type u_1} [Group G] {g : G} :
Subgroup.zpowers g ≠ ⊥ ↔ g ≠ 1
source
@[simp]
theorem AddSubgroup.zmultiples_zero_eq_bot {G : Type u_1} [AddGroup G] :
AddSubgroup.zmultiples 0 = ⊥
source
@[simp]
theorem Subgroup.zpowers_one_eq_bot {G : Type u_1} [Group G] :
Subgroup.zpowers 1 = ⊥
source
@[simp]
theorem AddSubgroup.zmultiples_neg {G : Type u_1} [AddGroup G] {g : G} :
AddSubgroup.zmultiples (-g) = AddSubgroup.zmultiples g
source
@[simp]
theorem Subgroup.zpowers_inv {G : Type u_1} [Group G] {g : G} :
Subgroup.zpowers g⁻¹ = Subgroup.zpowers g
source
theorem AddSubgroup.centralizer_closure {G : Type u_1} [AddGroup G] (S : Set G) :
AddSubgroup.centralizer ↑(AddSubgroup.closure S) = ⨅ g ∈ S, AddSubgroup.centralizer ↑(AddSubgroup.zmultiples g)
source
theorem Subgroup.centralizer_closure {G : Type u_1} [Group G] (S : Set G) :
Subgroup.centralizer ↑(Subgroup.closure S) = ⨅ g ∈ S, Subgroup.centralizer ↑(Subgroup.zpowers g)
source
theorem AddSubgroup.center_eq_iInf {G : Type u_1} [AddGroup G] (S : Set G) (hS : AddSubgroup.closure S = ⊤) :
AddSubgroup.center G = ⨅ g ∈ S, AddSubgroup.centralizer ↑(AddSubgroup.zmultiples g)
source
theorem Subgroup.center_eq_iInf {G : Type u_1} [Group G] (S : Set G) (hS : Subgroup.closure S = ⊤) :
Subgroup.center G = ⨅ g ∈ S, Subgroup.centralizer ↑(Subgroup.zpowers g)
source
theorem AddSubgroup.center_eq_infi' {G : Type u_1} [AddGroup G] (S : Set G) (hS : AddSubgroup.closure S = ⊤) :
AddSubgroup.center G = ⨅ (g : ↑S), AddSubgroup.centralizer ↑(AddSubgroup.zmultiples ↑g)
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.centralizer ↑(Subgroup.zpowers ↑g)
source
theorem AddSubgroup.closure_singleton_int_one_eq_top :
AddSubgroup.closure {1} = ⊤
source
theorem AddSubgroup.zmultiples_one_eq_top :
AddSubgroup.zmultiples 1 = ⊤