eq_liftHom — Mathlib

English

Unicity of liftHom: if g: S →ₐ[R] T satisfies g(h.root) = x, then g = h.liftHom x hx'.

Русский

Уникальность LiftHom: если g : S →ₐ[R] T удовлетворяет g(h.root) = x, тогда g = h.liftHom x hx'.

LaTeX

$$$ g = h.liftHom x hx' $$$

Lean4

/-- Unicity of `liftHom`: a map that agrees on `h.root` agrees with `liftHom` everywhere. -/
theorem eq_liftHom (g : S →ₐ[R] T) (hroot : g h.root = x) : g = h.liftHom x hx' :=
  AlgHom.ext (h.apply_eq_lift hx' g g.commutes hroot)

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