ofStarAlgHom — Mathlib

English

The underlying function of StarAlgEquiv.ofBijective is the bijective function itself.

Русский

Базовая функция StarAlgEquiv.ofBijective равна самой функции, заданной bijective.

LaTeX

$$$$ \operatorname{coe\_ofBijective} : (StarAlgEquiv.ofBijective f hf : A \to B) = f. $$$$

Lean4

/-- If a (unital or non-unital) star algebra morphism has an inverse, it is an isomorphism of
star algebras. -/
@[simps]
def ofStarAlgHom (f : F) (g : G) (h₁ : ∀ x, g (f x) = x) (h₂ : ∀ x, f (g x) = x) : A ≃⋆ₐ[R] B
    where
  toFun := f
  invFun := g
  left_inv := h₁
  right_inv := h₂
  map_add' := map_add f
  map_mul' := map_mul f
  map_smul' := map_smul f
  map_star' := map_star f

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