toAlgEquiv — Mathlib

English

The underlying AlgEquiv of the symmetry equals the symmetry of the underlying AlgEquiv.

Русский

Функционал подлежащей алгебраической эквивалентности симметрической операции равен симметрии исходной эквивалентности.

LaTeX

$$$$ e^{\mathrm{symm}}.toAlgEquiv = e.toAlgEquiv.symm. $$$$

Lean4

/-- Interpret a ⋆-algebra equivalence as an algebra equivalence. -/
def toAlgEquiv (f : A ≃⋆ₐ[R] B) : A ≃ₐ[R] B
    where
  toRingEquiv := f.toRingEquiv
  commutes' r := by simp_rw [Algebra.algebraMap_eq_smul_one', map_smul']; simp

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