addOrderOf_ofMul_eq_orderOf

Mathlib.GroupTheory.OrderOfElement

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

English

The additive order of an element equals the order of its multiplicative counterpart.

Русский

Порядок дополнения элемента равен порядку соответствующего элемента в умножении.

LaTeX

$$addOrderOf (Additive.ofMul x) = orderOf x$$

Lean4

@[simp]
theorem addOrderOf_ofMul_eq_orderOf (x : G) : addOrderOf (Additive.ofMul x) = orderOf x :=
  rfl

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

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

Разделы

Аффилиация

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