Theorems · Definition · commutative algebra

Ideal.Quotient.factor

{R : Type u} →
  [inst : Ring R] → {S T : Ideal R} → [inst_1 : S.IsTwoSided] → [inst_2 : T.IsTwoSided] → S ≤ T → R ⧸ S →+* R ⧸ T

The ring homomorphism from the quotient by a smaller ideal to the quotient by a larger ideal. This is the Ideal.Quotient version of Quot.Factor When the two ideals are of the form I^m and I^n and n ≤ m, please refer to the dedicated version Ideal.Quotient.factorPow.

Defined in

Mathlib.RingTheory.Ideal.Quotient.Defs

Cited by

33 results in Mathlib

Foundations

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

Assumes

RingIdeal.IsTwoSidedIdeal.IsTwoSided