orderOf_coe

Mathlib.GroupTheory.OrderOfElement

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

English

If a is an element of a subgroup H of G, then the order of a considered in G equals the order of a considered in H.

Русский

Пусть a принадлежит подгруппе H ⊆ G; тогда порядок a в G равен порядку a в H.

LaTeX

$$orderOf(a) = orderOf( (a : G) )$$

Lean4

@[to_additive (attr := norm_cast)]
theorem orderOf_coe (a : H) : orderOf (a : G) = orderOf a :=
  orderOf_injective H.subtype Subtype.coe_injective _

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

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

Разделы

Аффилиация

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