period_le_exponent — Mathlib

English

If 0 < exponent(M), then for all m ∈ M and a ∈ α, period(m,a) ≤ exponent(M). In particular, the period is uniformly bounded by the exponent of M.

Русский

Если 0 < экспонента(M), тогда для любых m ∈ M и a ∈ α период period(m,a) не превосходит экспоненту M.

LaTeX

$$0 < \operatorname{exponent}(M) \Rightarrow \forall m \in M, \forall a \in \alpha, \ \operatorname{period}(m,a) \le \operatorname{exponent}(M).$$

Lean4

@[to_additive]
theorem period_le_exponent (exp_pos : 0 < Monoid.exponent M) (m : M) (a : α) : period m a ≤ Monoid.exponent M :=
  Nat.le_of_dvd exp_pos (period_dvd_exponent m a)

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