ext_iff_val — Mathlib

English

In the homogeneous localization, equality is determined by the underlying value; two elements are equal if and only if their images under the canonical valuation map are equal.

Русский

В однородной локализации равенство определяется по базовой величине: два элемента равны тогда и только тогда, когда их образы под каноническим отображением равны.

LaTeX

$$$$ \forall f,g \in \mathrm{HomogeneousLocalization}(\mathcal{A}, x):\; f = g \iff f.val = g.val. $$$$

Lean4

theorem ext_iff_val (f g : HomogeneousLocalization 𝒜 x) : f = g ↔ f.val = g.val :=
  ⟨congr_arg val, fun e ↦ val_injective x e⟩

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