val_add — Mathlib

English

Let 𝒜 and x define the homogeneous localization; then the value map is additive: for any y1, y2 in the localization, (y1 + y2).val = y1.val + y2.val.

Русский

Пусть 𝒜 и x задают однородную локализацию; тогда отображение val сохраняет сложение: для любых y1, y2 в локализации выполняется (y1 + y2).val = y1.val + y2.val.

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_add : ∀ y1 y2 : HomogeneousLocalization 𝒜 x, (y1 + y2).val = y1.val + y2.val :=
  Quotient.ind₂' fun y1 y2 ↦ by rw [← mk_add, val_mk, val_mk, val_mk, Localization.add_mk]; rfl

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