orderOf_fst_dvd_orderOf

Mathlib.GroupTheory.OrderOfElement

URI: https://scilib.ai/kg/mathlib#orderOf_fst_dvd_orderOf

English

In a product x = (x1,x2), the order of the first component divides the order of x.

Русский

Для x=(x1,x2) из произведения ⟨orderOf x1⟩ делит orderOf x.

LaTeX

$$orderOf x.1 ∣ orderOf x$$

Lean4

@[to_additive]
theorem orderOf_fst_dvd_orderOf : orderOf x.1 ∣ orderOf x :=
  minimalPeriod_fst_dvd

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

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

Разделы

Аффилиация

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