orderOf

Mathlib.GroupTheory.OrderOfElement

URI: https://scilib.ai/kg/mathlib#Prod.orderOf

English

For x = (a,b) in a product of monoids, the order is the least common multiple of the orders: orderOf(x) = lcm(orderOf(a), orderOf(b)).

Русский

Для пары x=(a,b) в произведении моноидов orderOf(x) = lcm(orderOf(a), orderOf(b)).

LaTeX

$$orderOf (a,b) = (orderOf a) \operatorname{lcm} (orderOf b)$$

Lean4

@[to_additive]
protected theorem orderOf (x : α × β) : orderOf x = (orderOf x.1).lcm (orderOf x.2) :=
  minimalPeriod_prodMap _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru