realize_neg — Mathlib

English

The interpretation of the negation of a ring term under v is the negation of the interpretation of the term.

Русский

Интерпретация отрицания терма кольца под отображением v равна противоположному значению интерпретации терма.

LaTeX

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

Lean4

@[simp]
theorem realize_neg (x : ring.Term α) (v : α → R) : Term.realize v (-x) = -Term.realize v x := by
  simp [neg_def, funMap_neg]

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