instCoeLieHom — Mathlib

English

The coercion from AlgHom to LieHom is compatible with the underlying map; the LieHom obtained from an AlgHom has the same underlying function as the original AlgHom.

Русский

Приведение AlgHom к LieHom сохраняет подлинную функцию: соответствующий LieHom имеет ту же основную функцию, что и исходный AlgHom.

LaTeX

$$$$((f : A \to B)^{\text{Lie}}) = f.$$$$

Lean4

instance : Coe (A →ₐ[R] B) (A →ₗ⁅R⁆ B) :=
  ⟨toLieHom⟩

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