fst

Mathlib.GroupTheory.OrderOfElement

URI: https://scilib.ai/kg/mathlib#IsOfFinOrder.fst

English

If x = (a, b) has finite order in α × β, then a has finite order in α.

Русский

Если x = (a, b) имеет конечный порядок в α × β, то у a в α конечный порядок.

LaTeX

$$$\operatorname{FinOrd}((a,b)) \Rightarrow \operatorname{FinOrd}(a)$$$

Lean4

@[to_additive]
theorem fst {x : α × β} (hx : IsOfFinOrder x) : IsOfFinOrder x.1 :=
  hx.mono orderOf_fst_dvd_orderOf

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

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

Разделы

Аффилиация

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