toEndUnit_val

Mathlib.LinearAlgebra.RootSystem.Hom

URI: https://scilib.ai/kg/mathlib#RootPairing.Equiv.toEndUnit_val

English

There is an isomorphism to End(P)ˣ given by toEndUnit: Aut(P) ≃* (End(P))ˣ.

Русский

Существует изомеризм к группе единиц End(P)ˣ через отображение toEndUnit: Aut(P) ≃* (End(P))ˣ.

LaTeX

$$$\\\\mathrm{toEndUnit}(P): \\\\mathrm{Aut}(P) \\\\xrightarrow{\\\\sim} (\\\\mathrm{End}(P))^{\\\\times}.$$$

Lean4

theorem toEndUnit_val (P : RootPairing ι R M N) (g : Aut P) : (toEndUnit P g).val = g.toHom :=
  rfl

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

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

Разделы

Аффилиация

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