Theorems · Definition · commutative algebra
DoubleQuot.quotQuotEquivQuotOfLE
{R : Type u} → [inst : CommRing R] → {I J : Ideal R} → I ≤ J → (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J ≃+* R ⧸ JThe Third Isomorphism theorem for rings. See quotQuotEquivQuotSup for a version
that does not assume an inclusion of ideals.
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- RingHomstatement · cited by 10,189
- Idealstatement and proof · cited by 4,748
- HasQuotient.Quotientstatement · cited by 2,301
- RingEquivstatement · cited by 1,147
- Ideal.mapstatement · cited by 692
- Ideal.Quotient.mkstatement · cited by 610
- RingEquiv.transproof · cited by 54
- Ideal.quotEquivOfEqproof · cited by 15
- DoubleQuot.quotQuotEquivQuotSupproof · cited by 9
Cited by11
Results whose statement or proof uses this declaration.
- Ideal.Quotient.isUnit_mk_pow_iff_isUnit_mkproof · cited by 1
- Valued.integer.finite_quotient_maximalIdeal_pow_of_finite_residueFieldproof · cited by 1
- DoubleQuot.quotQuotEquivQuotOfLE.congr_simpstatement and proof · cited by 0
- DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMkstatement and proof · cited by 0
- DoubleQuot.quotQuotEquivQuotOfLE_quotQuotMkstatement · cited by 0
- DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mkstatement and proof · cited by 0
- DoubleQuot.quotQuotEquivQuotOfLE_symm_mkstatement · cited by 0
- DoubleQuot.quotQuotEquivQuotOfLEₐ_symm_toRingEquivstatement · cited by 0
- DoubleQuot.coe_quotQuotEquivQuotOfLEₐstatement · cited by 0
- DoubleQuot.coe_quotQuotEquivQuotOfLEₐ_symmstatement · cited by 0
- DoubleQuot.quotQuotEquivQuotOfLEₐ_toRingEquivstatement · cited by 0