realize_one — Mathlib

English

In any ring, the interpretation of the constant symbol 1 in the ring language is the multiplicative identity 1_R.

Русский

В кольце интерпретация константного символа 1 в языком кольца равна единице по умножению в этом кольце.

LaTeX

$$$ \\forall v:\\alpha \\to R ,\\; \\operatorname{Term.realize} v (1) = 1 $$$

Lean4

@[simp]
theorem realize_one (v : α → R) : Term.realize v (1 : ring.Term α) = 1 := by simp [one_def, funMap_one, constantMap]

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