toNonUnitalAlgHom_eq_coe — Mathlib

English

The underlying nonunital homomorphism of a unital algebra homomorphism is equal to the nonunital version obtained by forgetting the unit.

Русский

Подлежащий неединичный гомоморфизм алгебр единицы равен неединичному аналогу после забывания единицы.

LaTeX

$$$f^{\\!\\mathrm{toNonUnital}}=f$$$

Lean4

@[simp]
theorem toNonUnitalAlgHom_eq_coe (f : A →ₐ[R] B) : f.toNonUnitalAlgHom = f :=
  rfl

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