English
For a given root pairing P, the set Aut(P) of automorphisms forms a group under composition.
Русский
Для данного корневого парирования P множество автоморфизмов Aut(P) образует группу под операцией композиции.
LaTeX
$$$\\\\mathrm{Aut}(P) \\\\text{ is a group under }\\\\circ, \\\\text{ with identity } id_P \\\\text{ and inverse given by } f^{-1} = (\\\\text{symm } P\\\\, P \\\\text{ } f).$$$
Lean4
/-- Equivalences form a group. -/
instance (P : RootPairing ι R M N) : Group (RootPairing.Equiv P P)
where
mul := comp
mul_assoc := comp_assoc
one := id P
one_mul := id_comp P P
mul_one := comp_id P P
inv := symm P P
inv_mul_cancel
e := by
ext m
· rw [← weightEquiv_apply]
simp
· rw [← coweightEquiv_apply]
simp
· simp
