val_mul — Mathlib

English

In the homogeneous localization, the value map preserves multiplication: (y1·y2).val = y1.val · y2.val for any 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} \\cdot y_2.\\mathrm{val}$$$

Lean4

@[simp]
theorem val_mul : ∀ y1 y2 : HomogeneousLocalization 𝒜 x, (y1 * y2).val = y1.val * y2.val :=
  Quotient.ind₂' fun y1 y2 ↦ by rw [← mk_mul, val_mk, val_mk, val_mk, Localization.mk_mul]; rfl

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