minOrder_le_orderOf — Mathlib

English

If a ≠ 1 and a has finite order, then minOrder α is not larger than the order of a.

Русский

Если a ≠ 1 и a имеет конечный порядок, то minOrder α не превосходит order(a).

LaTeX

$$$\text{If } a \neq 1 \text{ and } IsOfFinOrder(a), \ \minOrder(\alpha) \le \operatorname{order}(a)$$$

Lean4

@[to_additive]
theorem minOrder_le_orderOf (ha : a ≠ 1) (ha' : IsOfFinOrder a) : minOrder α ≤ orderOf a :=
  le_minOrder.1 le_rfl ha ha'

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