lift_unique — Mathlib

English

If there exists g: RingQuot r →+* T with g ∘ mkRingHom r = f, then g = Lift ⟨f, w⟩ for the witness w.

Русский

Если существует g: RingQuot r →+* T с g ∘ mkRingHom r = f, тогда g = Lift ⟨f, w⟩ для некоторого доказательства w.

LaTeX

$$$\\forall f:\\, R \\to\\+* T,\\ w,\\ g:\\, RingQuot r \\to\\+* T,\\ h:\\ g \\circ mkRingHom r = f\\Rightarrow g = \\mathrm{lift}(\\langle f, w\\rangle)$$$

Lean4

theorem lift_unique (f : R →+* T) {r : R → R → Prop} (w : ∀ ⦃x y⦄, r x y → f x = f y) (g : RingQuot r →+* T)
    (h : g.comp (mkRingHom r) = f) : g = lift ⟨f, w⟩ := by
  ext
  simp [h]

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