isPGroup — Mathlib

English

The p-primary component is a p-group; i.e., every element in this component has order a power of p.

Русский

P-первичный компонент является p-группой; то есть каждый элемент компонента имеет порядок, равный степени p.

LaTeX

$$IsPGroup p (primaryComponent G p)$$

Lean4

/-- The `p`-primary component is a `p` group. -/
theorem isPGroup : IsPGroup p <| primaryComponent G p := fun g =>
  (propext exists_orderOf_eq_prime_pow_iff.symm).mpr (CommMonoid.primaryComponent.exists_orderOf_eq_prime_pow g)

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