orderOf_inv

Mathlib.GroupTheory.OrderOfElement

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

English

For any element x in a group, the order of x^{-1} equals the order of x.

Русский

Порядок x^{-1} равен порядку x в любой группе.

LaTeX

$$$\\operatorname{orderOf}(x^{-1}) = \\operatorname{orderOf}(x)$$$

Lean4

@[to_additive (attr := simp)]
theorem orderOf_inv (x : G) : orderOf x⁻¹ = orderOf x := by simp [orderOf_eq_orderOf_iff]

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

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

Разделы

Аффилиация

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