zero_apply

Mathlib.Algebra.Algebra.NonUnitalHom

URI: https://scilib.ai/kg/mathlib#NonUnitalAlgHom.zero_apply

English

Applying the zero morphism to any element yields zero.

Русский

Применение нулевого морфизма к любому элементу дает ноль.

LaTeX

$$$\forall a\in A,\ (0: A \to_{\mathrm{NonUnitalAlgHom}} B) a = 0$$$

Lean4

theorem zero_apply (a : A) : (0 : A →ₛₙₐ[φ] B) a = 0 :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru