Theorems · Theorem · commutative algebra

Ideal.Quotient.algHom_ext_iff

∀ {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 = g ↔ f.comp (Ideal.Quotient.mkₐ R₁ I) = g.comp (Ideal.Quotient.mkₐ R₁ I)

Defined in

Mathlib.RingTheory.TensorProduct.Quotient

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringRingAlgebraIdeal.IsTwoSidedSemiringAlgebra