val_mk — Mathlib

English

The value map applied to Away.mk is the canonical localization mk.

Русский

Значение, применённое к Away.mk, равно каноническому локализационному mk.

LaTeX

$$$$ (Away.mk 𝒜 hf n x hx).val = \mathrm{Localization.mk} x ⟨f^n, by use n⟩. $$$$

Lean4

@[simp]
theorem val_mk {d : ι} (n : ℕ) (hf : f ∈ 𝒜 d) (x : A) (hx : x ∈ 𝒜 (n • d)) :
    (Away.mk 𝒜 hf n x hx).val = Localization.mk x ⟨f ^ n, by use n⟩ :=
  rfl

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