conjAut_mul

Mathlib.CategoryTheory.Conj

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Iso.conjAut_mul

English

Definition: conjAut is the isomorphism between Aut X and Aut Y given by conjugation by α.

Русский

Определение: conjAut — изоморфизм между Aut X и Aut Y, задаваемый конъюгацией по α.

LaTeX

$$$\\mathrm{conjAut}: \\mathrm{Aut}(X) \\simeq^* \\mathrm{Aut}(Y)$$$

Lean4

@[simp]
theorem conjAut_mul (f g : Aut X) : α.conjAut (f * g) = α.conjAut f * α.conjAut g :=
  map_mul α.conjAut f g

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

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

Разделы

Аффилиация

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