smulZeroClass — Mathlib

English

The scalar action on MvPolynomial σ S1 is compatible with zero, i.e., it forms a SMulZeroClass: r • 0 = 0 (and often 0 • p = 0).

Русский

Действие скаляра на MvPolynomial σ S1 совместимо с нулём: любая скалярация нуля даёт ноль (и обычно 0 умножение даёт ноль).

LaTeX

$$$ r \cdot 0 = 0 \quad\text{and}\quad 0\cdot p = 0 $$

Lean4

instance smulZeroClass [CommSemiring S₁] [SMulZeroClass R S₁] : SMulZeroClass R (MvPolynomial σ S₁) :=
  AddMonoidAlgebra.smulZeroClass

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