period_dvd_exponent — Mathlib

English

Let M be a monoid acting on a set α. For every m ∈ M and a ∈ α, the period of a under m, denoted period(m,a), divides the exponent of M. In other words, period(m,a) is a divisor of the exponent of M.

Русский

Пусть M — моноид, действующий на множество α. Для любых элементов m ∈ M и a ∈ α период действия period(m,a) делится на экспоненту моноида M; то есть period(m,a) делится на экспоненту M.

LaTeX

$$$\operatorname{period}(m,a) \mid \operatorname{exponent}(M)$$$

Lean4

@[to_additive]
theorem period_dvd_exponent (m : M) (a : α) : period m a ∣ Monoid.exponent M := by
  rw [← pow_smul_eq_iff_period_dvd, Monoid.pow_exponent_eq_one, one_smul]

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