Theorems · Theorem · commutative algebra

Ideal.Quotient.algHom_ext

∀ (R₁ : Type u_1) {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] {I : Ideal A}
  [inst_3 : I.IsTwoSided] {S : Type u_5} [inst_4 : Semiring S] [inst_5 : Algebra R₁ S] ⦃f g : A ⧸ I →ₐ[R₁] S⦄,
  f.comp (Ideal.Quotient.mkₐ R₁ I) = g.comp (Ideal.Quotient.mkₐ R₁ I) → f = g

Defined in

Mathlib.RingTheory.Ideal.Quotient.Operations

Cited by

6 results in Mathlib

Foundations

Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringRingAlgebraIdeal.IsTwoSidedSemiringAlgebra