smeval_congr — Mathlib

English

If f = g and x = y, then f.smeval x = g.smeval y. The smeval map respects equality of both the polynomials and the units.

Русский

Если f = g и x = y, то f.smeval x = g.smeval y. Карта smeval сохраняет равенство как полиномов, так и операций оценки.

LaTeX

$$$ f = g \; \Rightarrow \; x = y \; \Rightarrow \; f.smeval(x) = g.smeval(y) $$$

Lean4

theorem smeval_congr : f = g → x = y → f.smeval x = g.smeval y := by rintro rfl rfl; rfl

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