LeanPool.OrderPQ.TorsionBy

def Subgroup.torsionBy' (α : Type u_1) [CommGroup α] (d : ℕ) : Subgroup α

The subgroup of elements a of a commutative group α satisfying a ^ d = 1.

Equations

• Subgroup.torsionBy' α d = { carrier := {a : α | a ^ d = 1}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

def AddSubgroup.torsionBy' (α : Type u_1) [AddCommGroup α] (d : ℕ) : AddSubgroup α

The subgroup of elements a of an additive commutative group α satisfying d • a = 0.

Equations

• AddSubgroup.torsionBy' α d = { carrier := {a : α | d • a = 0}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem Subgroup.coe_torsionBy' (α : Type u_1) [CommGroup α] (d : ℕ) : ↑(torsionBy' α d) = {a : α | a ^ d = 1}

@[simp]

theorem AddSubgroup.coe_torsionBy' (α : Type u_1) [AddCommGroup α] (d : ℕ) : ↑(torsionBy' α d) = {a : α | d • a = 0}

@[simp]

theorem Subgroup.mem_torsionBy' {α : Type u_1} [CommGroup α] (d : ℕ) (a : α) : a ∈ torsionBy' α d ↔ a ^ d = 1

@[simp]

theorem AddSubgroup.mem_torsionBy' {α : Type u_1} [AddCommGroup α] (d : ℕ) (a : α) : a ∈ torsionBy' α d ↔ d • a = 0