toEndUnit_inv — Mathlib

English

The inverse in End(P)ˣ corresponds to the inverse automorphism under the isomorphism to End(P)ˣ.

Русский

Обратный элемент в End(P)ˣ соответствует обратному автоморфизму в рамках изоморфизма к End(P)ˣ.

LaTeX

$$$(toEndUnit(P)\\, g)^{-1} = (\\\\mathrm{symm}(P,P,g)).toHom.$$$

Lean4

theorem toEndUnit_inv (P : RootPairing ι R M N) (g : Aut P) : (toEndUnit P g).inv = (symm P P g).toHom :=
  rfl

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