English
The p-primary component of a commutative monoid G is the submonoid of elements whose order is a power of p.
Русский
p-основной компонент коммутативного моноида G — это подп Monoid элементов, чьи порядки являются степенями p.
LaTeX
$$def primaryComponent : Submonoid G$$
Lean4
/-- The `p`-primary component is the submonoid of elements with order prime-power of `p`. -/
@[to_additive (attr := simps) /-- The `p`-primary component is the submonoid of elements with additive
order prime-power of `p`. -/
]
def primaryComponent : Submonoid G where
carrier := {g | ∃ n : ℕ, orderOf g = p ^ n}
one_mem' := ⟨0, by rw [pow_zero, orderOf_one]⟩
mul_mem' hg₁
hg₂ :=
exists_orderOf_eq_prime_pow_iff.mpr <|
by
obtain ⟨m, hm⟩ := exists_orderOf_eq_prime_pow_iff.mp hg₁
obtain ⟨n, hn⟩ := exists_orderOf_eq_prime_pow_iff.mp hg₂
exact ⟨m + n, by rw [mul_pow, pow_add, pow_mul, hm, one_pow, Monoid.one_mul, mul_comm, pow_mul, hn, one_pow]⟩
