inv_left_iff₀

Mathlib.Algebra.GroupWithZero.Commute

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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