realize_mul — Mathlib

English

The interpretation of a product of two ring terms under a valuation v is the product of their interpretations.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem realize_mul (x y : ring.Term α) (v : α → R) : Term.realize v (x * y) = Term.realize v x * Term.realize v y := by
  simp [mul_def, funMap_mul]

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