instZero — Mathlib

English

There exists a zero morphism A → B in nonunital algebra homomorphisms, given by sending every element to 0 and preserving addition, scalar action, and multiplication in the appropriate sense.

Русский

Существует нулевой гомоморфизм A → B в классе неполунальных алгебра-гомоморфизмов, который отправляет каждый элемент в 0 и сохраняет сложение, действие скаляра и умножение в соответствующем смысле.

LaTeX

$$$\exists f: A \to_{\mathrm{NonUnitalAlgHom}} B\text{ with } f(a)=0\ \forall a,\ f(a+b)=f(a)+f(b),\ f(r\cdot a)=r\cdot f(a),\ f(ab)=f(a)f(b)$$$

Lean4

instance : Zero (A →ₛₙₐ[φ] B) :=
  ⟨{ (0 : A →ₑ+[φ] B) with map_mul' := by simp }⟩

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