orderOf_mk

Mathlib.GroupTheory.OrderOfElement

URI: https://scilib.ai/kg/mathlib#Subgroup.orderOf_mk

English

The order of the element a in the subgroup H, when viewed as an element of G, equals the order of a in G.

Русский

Порядок элемента a в подпгруппе H при его восприятии как элемента G равен порядку a в G.

LaTeX

$$orderOf(⟨a, ha⟩) = orderOf(a)$$

Lean4

@[to_additive (attr := simp)]
theorem orderOf_mk (a : G) (ha) : orderOf (⟨a, ha⟩ : H) = orderOf a :=
  (orderOf_coe _).symm

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

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

Разделы

Аффилиация

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