units_inv_left_iff

Mathlib.Algebra.Group.Commute.Units

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

English

Commute (↑u^{-1}) a ↔ Commute (↑u) a.

Русский

Commute (↑u^{-1}) a эквивалентно Commute (↑u) a.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem units_inv_left_iff : Commute (↑u⁻¹) a ↔ Commute (↑u) a :=
  SemiconjBy.units_inv_symm_left_iff

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

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

Разделы

Аффилиация

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