snd

Mathlib.GroupTheory.OrderOfElement

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

English

If x = (a, b) has finite order, then b has finite order.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem snd {x : α × β} (hx : IsOfFinOrder x) : IsOfFinOrder x.2 :=
  hx.mono orderOf_snd_dvd_orderOf

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

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

Разделы

Аффилиация

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