English
For any element g in the p-primary component of a commutative monoid, its order is a power of p; i.e., there exists n such that orderOf g = p^n.
Русский
Для любого элемента g в p-первичном компоненте коммутативного моноида порядок элемента равен степени p: существует n, такое что orderOf(g) = p^n.
LaTeX
$$$\forall g \in CommMonoid.primaryComponent\, G\, p,\; \exists n \in \mathbb{N}, \operatorname{orderOf} g = p^{n}.$$$
Lean4
/-- Elements of the `p`-primary component have order `p^n` for some `n`. -/
@[to_additive primaryComponent.exists_orderOf_eq_prime_nsmul /--
Elements of the `p`-primary component have additive order `p^n` for some `n` -/
]
theorem exists_orderOf_eq_prime_pow (g : CommMonoid.primaryComponent G p) : ∃ n : ℕ, orderOf g = p ^ n :=
by
obtain ⟨_, hn⟩ := g.property
rw [orderOf_submonoid g] at hn
exact ⟨_, hn⟩
