coweightHom_op — Mathlib

English

There is an isomorphism between Aut P and units of End P, with explicit inverses given by the Symm construction.

Русский

Существует изоморфизм между Aut P и единицами End P, где явные обратные элементы даны через конструкцию Symm.

LaTeX

$$$\\\\mathrm{Aut}(P) \\\\cong (\mathrm{End}(P))^{\\\\times}.$$$

Lean4

theorem coweightHom_op {P : RootPairing ι R M N} (g : Aut P) :
    MulOpposite.unop (coweightHom P g) = coweightEquiv P P g :=
  rfl

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