Documentation

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

Subgroup G

The subgroup generated by an element.

Instances For

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

AddSubgroup G

The additive subgroup generated by an element.

Instances For

@[simp]

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

g ∈ zpowers g

@[simp]

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

g ∈ zmultiples g

theorem Subgroup.coe_zpowers {G : Type u_1} [Group G] (g : G) :

↑(zpowers g) = Set.range fun (x : ℤ) => g ^ x

theorem AddSubgroup.coe_zmultiples {G : Type u_1} [AddGroup G] (g : G) :

↑(zmultiples g) = Set.range fun (x : ℤ) => x • g

@[implicit_reducible]

noncomputable instance Subgroup.decidableMemZPowers {G : Type u_1} [Group G] {a : G} :

DecidablePred fun (x : G) => x ∈ zpowers a

@[implicit_reducible]

noncomputable instance AddSubgroup.decidableMemZMultiples {G : Type u_1} [AddGroup G] {a : G} :

DecidablePred fun (x : G) => x ∈ zmultiples a

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

zpowers g = closure {g}

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

zmultiples g = closure {g}

theorem Subgroup.mem_zpowers_iff {G : Type u_1} [Group G] {g h : G} :

h ∈ zpowers g ↔ ∃ (k : ℤ), g ^ k = h

theorem AddSubgroup.mem_zmultiples_iff {G : Type u_1} [AddGroup G] {g h : G} :

h ∈ zmultiples g ↔ ∃ (k : ℤ), k • g = h

@[simp]

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

g ^ k ∈ zpowers g

@[simp]

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

k • g ∈ zmultiples g

@[simp]

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

g ^ k ∈ zpowers g

@[simp]

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

k • g ∈ zmultiples g

@[simp]

theorem Subgroup.forall_zpowers {G : Type u_1} [Group G] {x : G} {p : ↥(zpowers x) → Prop} :

(∀ (g : ↥(zpowers x)), p g) ↔ ∀ (m : ℤ), p ⟨x ^ m, ⋯⟩

@[simp]

theorem AddSubgroup.forall_zmultiples {G : Type u_1} [AddGroup G] {x : G} {p : ↥(zmultiples x) → Prop} :

(∀ (g : ↥(zmultiples x)), p g) ↔ ∀ (m : ℤ), p ⟨m • x, ⋯⟩

@[simp]

theorem Subgroup.exists_zpowers {G : Type u_1} [Group G] {x : G} {p : ↥(zpowers x) → Prop} :

(∃ (g : ↥(zpowers x)), p g) ↔ ∃ (m : ℤ), p ⟨x ^ m, ⋯⟩

@[simp]

theorem AddSubgroup.exists_zmultiples {G : Type u_1} [AddGroup G] {x : G} {p : ↥(zmultiples x) → Prop} :

(∃ (g : ↥(zmultiples x)), p g) ↔ ∃ (m : ℤ), p ⟨m • x, ⋯⟩

theorem Subgroup.forall_mem_zpowers {G : Type u_1} [Group G] {x : G} {p : G → Prop} :

(∀ g ∈ zpowers x, p g) ↔ ∀ (m : ℤ), p (x ^ m)

theorem AddSubgroup.forall_mem_zmultiples {G : Type u_1} [AddGroup G] {x : G} {p : G → Prop} :

(∀ g ∈ zmultiples x, p g) ↔ ∀ (m : ℤ), p (m • x)

theorem Subgroup.exists_mem_zpowers {G : Type u_1} [Group G] {x : G} {p : G → Prop} :

(∃ g ∈ zpowers x, p g) ↔ ∃ (m : ℤ), p (x ^ m)

theorem AddSubgroup.exists_mem_zmultiples {G : Type u_1} [AddGroup G] {x : G} {p : G → Prop} :

(∃ g ∈ zmultiples x, p g) ↔ ∃ (m : ℤ), p (m • 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)

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

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

instance Subgroup.zpowers_isMulCommutative {G : Type u_1} [Group G] (g : G) :

IsMulCommutative ↥(zpowers g)

instance AddSubgroup.zmultiples_isAddCommutative {G : Type u_1} [AddGroup G] (g : G) :

IsAddCommutative ↥(zmultiples g)

@[simp]

theorem Subgroup.zpowers_le {G : Type u_1} [Group G] {g : G} {H : Subgroup G} :

zpowers g ≤ H ↔ g ∈ H

@[simp]

theorem AddSubgroup.zmultiples_le {G : Type u_1} [AddGroup G] {g : G} {H : AddSubgroup G} :

zmultiples g ≤ H ↔ g ∈ H

theorem Subgroup.zpowers_le_of_mem {G : Type u_1} [Group G] {g : G} {H : Subgroup G} :

g ∈ H → 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 → zmultiples g ≤ H

@[simp]

theorem Subgroup.zpowers_eq_bot {G : Type u_1} [Group G] {g : G} :

zpowers g = ⊥ ↔ g = 1

@[simp]

theorem AddSubgroup.zmultiples_eq_bot {G : Type u_1} [AddGroup G] {g : G} :

zmultiples g = ⊥ ↔ g = 0

theorem Subgroup.zpowers_ne_bot {G : Type u_1} [Group G] {g : G} :

zpowers g ≠ ⊥ ↔ g ≠ 1

theorem AddSubgroup.zmultiples_ne_bot {G : Type u_1} [AddGroup G] {g : G} :

zmultiples g ≠ ⊥ ↔ g ≠ 0

@[simp]

theorem Subgroup.zpowers_one_eq_bot {G : Type u_1} [Group G] :

zpowers 1 = ⊥

@[simp]

theorem AddSubgroup.zmultiples_zero_eq_bot {G : Type u_1} [AddGroup G] :

zmultiples 0 = ⊥

@[simp]

theorem Subgroup.zpowers_inv {G : Type u_1} [Group G] {g : G} :

zpowers g⁻¹ = zpowers g

@[simp]

theorem AddSubgroup.zmultiples_neg {G : Type u_1} [AddGroup G] {g : G} :

zmultiples (-g) = zmultiples g

theorem Int.zmultiples_natAbs (a : ℤ) :

AddSubgroup.zmultiples ↑a.natAbs = AddSubgroup.zmultiples a