units_inv_right

Mathlib.Algebra.Group.Commute.Units

URI: https://scilib.ai/kg/mathlib#Commute.units_inv_right

English

If Commute a with a unit u, then a commutes with u^{-1} (the inverse unit).

Русский

Если a коммутирует с единицей-обратной, то a коммутирует с обратной единицей.

LaTeX

$$$Commute(a, u) \Rightarrow Commute(a, ↑u^{-1})$$$

Lean4

@[to_additive]
theorem units_inv_right : Commute a u → Commute a ↑u⁻¹ :=
  SemiconjBy.units_inv_right

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

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

Разделы

Аффилиация

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