Theorems · Theorem · commutative algebra

Ideal.quotientMap_algebraMap

∀ {R₁ : Type u_1} {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] {S : Type v}
  [inst_3 : Ring S] {J : Ideal A} {I : Ideal S} [inst_4 : I.IsTwoSided] [inst_5 : J.IsTwoSided] {f : A →+* S}
  {H : J ≤ Ideal.comap f I} {x : R₁},
  (Ideal.quotientMap I f H) ((algebraMap R₁ (A ⧸ J)) x) = (Ideal.Quotient.mk I) (f ((algebraMap R₁ A) x))

Defined in

Mathlib.RingTheory.Ideal.Quotient.Operations

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringRingAlgebraRingIdeal.IsTwoSidedIdeal.IsTwoSided