eq_lift — Mathlib

English

Unicity of lift: if g : S → T agrees on R and sends h.root to x, then g = h.lift i x hx.

Русский

Уникальность лифта: если g : S → T совпадает на R и отправляет h.root в x, то g равен h.lift i x hx.

LaTeX

$$$ g = h.lift i x hx $$$

Lean4

/-- Unicity of `lift`: a map that agrees on `R` and `h.root` agrees with `lift` everywhere. -/
theorem eq_lift (g : S →+* T) (hmap : ∀ a, g (algebraMap R S a) = i a) (hroot : g h.root = x) : g = h.lift i x hx :=
  RingHom.ext (h.apply_eq_lift hx g hmap hroot)

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