orderOf_snd_dvd_orderOf — Mathlib

English

Let α and β be monoids and x = (a, b) ∈ α × β. Then the order of b divides the order of x, i.e. ord(b) | ord((a, b)). In particular, ord((a, b)) = lcm(ord(a), ord(b)).

Русский

Пусть α и β — моноиды, элемент x = (a, b) ∈ α × β. Порядок b делится на порядок x, то есть ord(b) | ord((a, b)). В частности ord((a, b)) = lcm(ord(a), ord(b)).

LaTeX

$$$\operatorname{order}(b) \\mid \operatorname{order}((a,b))$$$

Lean4

@[to_additive]
theorem orderOf_snd_dvd_orderOf : orderOf x.2 ∣ orderOf x :=
  minimalPeriod_snd_dvd

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