val_sub — Mathlib

English

The val function respects subtraction: (y1 - y2).val = y1.val - y2.val for all y1,y2.

Русский

Функция val сохраняет вычитание: (y1 - y2).val = y1.val - y2.val для любых y1,y2.

LaTeX

$$$\\forall y_1,y_2 \\in \\mathrm{HomogeneousLocalization}(\\mathcal{A},x),\\; (y_1 - y_2).\\mathrm{val} = y_1.\\mathrm{val} - y_2.\\mathrm{val}$$$

Lean4

@[simp]
theorem val_sub (y1 y2 : HomogeneousLocalization 𝒜 x) : (y1 - y2).val = y1.val - y2.val := by
  rw [sub_eq_add_neg, ← val_neg, ← val_add]; rfl

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