embedding — Mathlib

English

An embedding maps a homogeneous fraction p = (num, den) to the localized element p.num/p.den in A_x.

Русский

Встраивание переводит однородную дробь p = (num, den) в элемент p.num/p.den в A_x.

LaTeX

$$$\\mathrm{embedding}(p) = \\mathrm{Localization.mk}(p.\\mathrm{num}, \\langle p.\\mathrm{den}, p.\\mathrm{den\\,mem} \\rangle)$$$

Lean4

/-- For `x : prime ideal of A` and any `p : NumDenSameDeg 𝒜 x`, or equivalent a numerator and a
denominator of the same degree, we get an element `p.num / p.den` of `Aₓ`.
-/
def embedding (p : NumDenSameDeg 𝒜 x) : at x :=
  Localization.mk p.num ⟨p.den, p.den_mem⟩

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