trans

Mathlib.Algebra.Group.Conj

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

English

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

Русский

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

LaTeX

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

Lean4

@[trans]
theorem trans {a b c : α} : IsConj a b → IsConj b c → IsConj a c
  | ⟨c₁, hc₁⟩, ⟨c₂, hc₂⟩ => ⟨c₂ * c₁, hc₂.mul_left hc₁⟩

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

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

Разделы

Аффилиация

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