orderOf_ofAdd_eq_addOrderOf

Mathlib.GroupTheory.OrderOfElement

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

English

The additive order of the image of x under Additive.ofMul equals the order of x.

Русский

Порядок дополнения образа x под Additive.ofMul равен порядку x.

LaTeX

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

Lean4

@[simp]
theorem orderOf_ofAdd_eq_addOrderOf {α : Type*} [AddMonoid α] (a : α) :
    orderOf (Multiplicative.ofAdd a) = addOrderOf a :=
  rfl

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

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

Разделы

Аффилиация

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