inv_right_iff₀

Mathlib.Algebra.GroupWithZero.Commute

URI: https://scilib.ai/kg/mathlib#Commute.inv_right_iff₀

English

In a group with zero, a commutes with b⁻¹ iff a commutes with b.

Русский

В группе с нулём a коммутирует с b⁻¹ тогда и только тогда, когда a коммутирует с b.

LaTeX

$$$Commute a b^{-1} \leftrightarrow Commute a b$$$

Lean4

@[simp]
theorem inv_right_iff₀ : Commute a b⁻¹ ↔ Commute a b :=
  SemiconjBy.inv_right_iff₀

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

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

Разделы

Аффилиация

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