coe_algHom — Mathlib

English

An algebra equivalence e induces an algebra homomorphism with the same action on elements, and the underlying function respects the algebra structure.

Русский

Эквивалентность A1 ≃ₐ[R] A2 порождает алгебра-гомоморфизм со значением на элементах и сохраняет алгебраическую структуру.

LaTeX

$$$ e : A_1 \simeq_{R} A_2 \Rightarrow e.toAlgHom: A_1 \to_{R} A_2 $$$

Lean4

@[simp, norm_cast]
theorem coe_algHom : DFunLike.coe (e.toAlgHom) = DFunLike.coe e :=
  rfl

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