aut — Mathlib

English

The star-algebra automorphisms form a group under composition with inverse given by the symm.

Русский

⋆-алгебра автоморфизмы образуют группу по композиции; обратный задан симмметрией.

LaTeX

$$$$ \text{Aut}_{\star}^{S}(R) \; \text{is a group with multiplication } f \cdot g = g.trans f, \text{ identity } \mathrm{id}, \text{ inverse } f^{-1} = f^{\mathrm{symm}}. $$$$

Lean4

@[simps -isSimp one mul]
instance aut : Group (R ≃⋆ₐ[S] R) where
  one := refl
  mul a b := b.trans a
  one_mul _ := rfl
  mul_one _ := rfl
  mul_assoc _ _ _ := rfl
  inv f := f.symm
  inv_mul_cancel f := ext <| symm_apply_apply f

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