Subgroups generated by an element

Tags

subgroup, subgroups

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

The subgroup generated by an element.

Equations

• Subgroup.zpowers g = Subgroup.copy (MonoidHom.range ((zpowersHom G) g)) (Set.range fun (x : ℤ) => g ^ x) (_ : (Set.range fun (x : ℤ) => g ^ x) = Set.range fun (x : ℤ) => g ^ x)

@[simp]

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

theorem Subgroup.coe_zpowers {G : Type u_1} [Group G] (g : G) : ↑(Subgroup.zpowers g) = Set.range fun (x : ℤ) => g ^ x

noncomputable instance Subgroup.decidableMemZPowers {G : Type u_1} [Group G] {a : G} : DecidablePred fun (x : G) => x ∈ Subgroup.zpowers a

Equations

• Subgroup.decidableMemZPowers = Classical.decPred fun (x : G) => x ∈ Subgroup.zpowers a

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[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 { val := x ^ m, property := (_ : ∃ (y : ℤ), (fun (x_1 : ℤ) => x ^ x_1) y = x ^ m) }

@[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 { val := x ^ m, property := (_ : ∃ (y : ℤ), (fun (x_1 : ℤ) => x ^ x_1) y = x ^ m) }

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)

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)

instance Subgroup.instCountableSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupZpowers {G : Type u_1} [Group G] (a : G) : Countable ↥(Subgroup.zpowers a)

Equations

• (_ : Countable ↥(Subgroup.zpowers a)) = (_ : Countable ↥(MonoidHom.range ((zpowersHom G) a)))

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

The subgroup generated by an element.

Equations

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

@[simp]

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

@[simp]

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

theorem AddSubgroup.coe_zmultiples {G : Type u_1} [AddGroup G] (g : G) : ↑(AddSubgroup.zmultiples g) = Set.range fun (x : ℤ) => x • g

noncomputable instance AddSubgroup.decidableMemZMultiples {G : Type u_1} [AddGroup G] {a : G} : DecidablePred fun (x : G) => x ∈ AddSubgroup.zmultiples a

Equations

• AddSubgroup.decidableMemZMultiples = Classical.decPred fun (x : G) => x ∈ AddSubgroup.zmultiples a

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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)

@[simp]

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

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)

instance AddSubgroup.instCountableSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupZmultiples {A : Type u_2} [AddGroup A] (a : A) : Countable ↥(AddSubgroup.zmultiples a)

Equations

• (_ : Countable ↥(AddSubgroup.zmultiples a)) = (_ : Countable ↥(AddMonoidHom.range ((zmultiplesHom A) a)))

@[simp]

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

@[simp]

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

@[simp]

theorem Int.range_castAddHom {A : Type u_4} [AddGroupWithOne A] : AddMonoidHom.range (Int.castAddHom A) = AddSubgroup.zmultiples 1

@[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)

@[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)

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

@[simp]

theorem Int.zmultiples_one : AddSubgroup.zmultiples 1 = ⊤

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))

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))

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

Equations

• (_ : motive x) = (_ : motive x)

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

Equations

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

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

Equations

• (_ : Subgroup.IsCommutative (Subgroup.zpowers g)) = (_ : Subgroup.IsCommutative (Subgroup.zpowers g))

@[simp]

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

@[simp]

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

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.

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.

@[simp]

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

@[simp]

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

theorem AddSubgroup.zmultiples_ne_bot {G : Type u_1} [AddGroup G] {g : G} : AddSubgroup.zmultiples g ≠ ⊥ ↔ g ≠ 0

theorem Subgroup.zpowers_ne_bot {G : Type u_1} [Group G] {g : G} : Subgroup.zpowers g ≠ ⊥ ↔ g ≠ 1

@[simp]

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

@[simp]

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

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)

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)

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)

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)

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)

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)