ofBijective — Mathlib

English

The star-algebra automorphisms of R form a group under composition.

Русский

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

LaTeX

$$$$ \text{Aut}_{\star}^{S}(R) \text{ is a group under composition.} $$$$

Lean4

/-- Promote a bijective star algebra homomorphism to a star algebra equivalence. -/
noncomputable def ofBijective (f : F) (hf : Function.Bijective f) : A ≃⋆ₐ[R] B :=
  {
    RingEquiv.ofBijective f (hf : Function.Bijective
          (f : A → B)) with
    toFun := f
    map_star' := map_star f
    map_smul' := map_smul f }

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