primaryComponent — Mathlib

English

The p-primary component is the subgroup consisting of elements whose orders are prime-powers of p.

Русский

p-первичный компонент является подгруппой, состоящей из элементов, чьи порядки являются степенями p.

LaTeX

$$$\text{primaryComponent}(G,p) :\text{Subgroup } G$$$

Lean4

/-- The `p`-primary component is the subgroup of elements with order prime-power of `p`. -/
@[to_additive (attr := simps!) /-- The `p`-primary component is the subgroup of elements with additive order
          prime-power of `p`. -/
    ]
def primaryComponent : Subgroup G :=
  { CommMonoid.primaryComponent G p with inv_mem' := fun {g} ⟨n, hn⟩ => ⟨n, (orderOf_inv g).trans hn⟩ }

Похожие утверждения