lift_eq — Mathlib

English

For x ∈ R, lift hg applied to algebraMap_R_S x equals g(x). In other words, the lift extends g on the base ring.

Русский

Для x ∈ R отображение lift hg от algebraMap_R_S(x) равно g(x). Иными словами, lift продолжает g на базовом кольце.

LaTeX

$$$ \\mathrm{lift}\\;hg\\ ((\\mathrm{algebraMap}_{R,S})\, x) = g(x). $$$

Lean4

@[simp]
theorem lift_eq (x : R) : lift hg ((algebraMap R S) x) = g x :=
  (toLocalizationMap M S).lift_eq _ _

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