realize_zero — Mathlib

English

The interpretation of the constant 0 in the ring term language is 0 in the target ring under any valuation.

Русский

Интерпретация константы 0 в языке кольца равна нулю в целевом кольце под любой шкалировке.

LaTeX

$$$\operatorname{Term.realize}(v, 0) = 0.$$$

Lean4

@[simp]
theorem realize_zero (v : α → R) : Term.realize v (0 : ring.Term α) = 0 := by simp [zero_def, funMap_zero, constantMap]

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