instZero

Mathlib.RingTheory.PolynomialLaw.Basic

URI: https://scilib.ai/kg/mathlib#PolynomialLaw.instZero

English

There exists a zero polynomial law sending every input to 0.

Русский

Существует нулевой полиномальный закон, отправляющий любой ввод в ноль.

LaTeX

$$$0 : M \to_p_l[R] N$ is defined by $(0)^{\mathrm{toFun}'}S = 0$ for all S.$$

Lean4

instance : Zero (M →ₚₗ[R] N) :=
  ⟨{ toFun' _ := 0 }⟩

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

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

Разделы

Аффилиация

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