mk' — Mathlib

English

mk' embeds an integral element of B into A as an element of the integral closure, preserving the algebra map to B.

Русский

mk' отображает интегральный элемент B в A так, чтобы образ по алгебраическому отображению совпал с исходным элементом в B.

LaTeX

$$$\text{algebraMap } A B (\mathrm{mk'}\; A\; x\; hx) = x$$$

Lean4

/-- If `x : B` is integral over `R`, then it is an element of the integral closure of `R` in `B`. -/
noncomputable def mk' (x : B) (hx : IsIntegral R x) : A :=
  Classical.choose (isIntegral_iff.mp hx)

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