ofAlgEquiv — Mathlib

English

Upgrade an algebra equivalence to a star-algebra equivalence given preservation of star.

Русский

Преобразование алгебраической эквивалентности в ⋆-эквивалентность при условии сохранения операции star.

LaTeX

$$$$ \text{ofAlgEquiv} : (f : A \simeq_{\mathrm{alg}} B) \to (A \simeq_{\star}^{R} B) $$$$

Lean4

/-- Upgrade an algebra equivalence to a ⋆-algebra equivalence given that it preserves the
`star` operation. -/
def ofAlgEquiv (f : A ≃ₐ[R] B) (map_star : ∀ x, f (star x) = star (f x)) : A ≃⋆ₐ[R] B
    where
  toRingEquiv := f.toRingEquiv
  map_smul' := f.toLinearEquiv.map_smul
  map_star' := map_star

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