Theorems · Theorem · commutative algebra

RingQuot.lift_unique

∀ {R : Type uR} [inst : Semiring R] {T : Type uT} [inst_1 : Semiring T] (f : R →+* T) {r : R → R → Prop}
  (w : ∀ ⦃x y : R⦄, r x y → f x = f y) (g : RingQuot r →+* T),
  g.comp (RingQuot.mkRingHom r) = f → g = RingQuot.lift ⟨f, w⟩

Defined in

Mathlib.Algebra.RingQuot

Cited by

1 results in Mathlib

Foundations

Depth 46 from the axioms · uses propext, Quot.sound

Assumes

SemiringSemiring