English
The p-primary component is a p-group; that is, every element in the p-primary component has order a power of p.
Русский
p-первичный компонент является p-группой; каждый элемент p-первичного компонента имеет порядок, равный степени p.
LaTeX
$$$\text{IsPGroup}(p, \operatorname{primaryComponent}(G,p)).$$$
Lean4
/-- Torsion submonoids of a torsion submonoid are isomorphic to the submonoid. -/
@[to_additive (attr := simp) AddCommMonoid.Torsion.ofTorsion /--
Additive torsion submonoids of an additive torsion submonoid are
isomorphic to the submonoid. -/
]
def ofTorsion : torsion (torsion G) ≃* torsion G :=
Monoid.IsTorsion.torsionMulEquiv CommMonoid.torsion.isTorsion
