symm

Mathlib.Algebra.Group.Conj

URI: https://scilib.ai/kg/mathlib#IsConj.symm

English

If IsConj(a,b) then IsConj(b,a).

Русский

Если a конъугировано b, то b конъугировано a.

LaTeX

$$$IsConj(a,b) \\Rightarrow IsConj(b,a)$$$

Lean4

@[symm]
theorem symm {a b : α} : IsConj a b → IsConj b a
  | ⟨c, hc⟩ => ⟨c⁻¹, hc.units_inv_symm_left⟩

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

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

Разделы

Аффилиация

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