toAlgEquiv_trans — Mathlib

English

The AlgEquiv associated to a composite of StarAlgEquivs equals the composite of their AlgEquivs.

Русский

AlgEquiv, соответствующий композиту StarAlgEquiv, равен композиту их AlgEquiv.

LaTeX

$$$$ (f \xrightarrow{.trans} g).toAlgEquiv = f.toAlgEquiv.trans g.toAlgEquiv. $$$$

Lean4

@[simp]
theorem toAlgEquiv_trans {C : Type*} [Semiring C] [Algebra R C] [Star C] (f : A ≃⋆ₐ[R] B) (g : B ≃⋆ₐ[R] C) :
    (f.trans g).toAlgEquiv = f.toAlgEquiv.trans g.toAlgEquiv :=
  rfl

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