Theorems · Definition · commutative algebra
Ideal.quotEquivOfEq
{R : Type u} →
[inst : Ring R] → {I J : Ideal R} → [inst_1 : I.IsTwoSided] → [inst_2 : J.IsTwoSided] → I = J → R ⧸ I ≃+* R ⧸ JQuotienting by equal ideals gives equivalent rings.
See also Submodule.quotEquivOfEq and Ideal.quotientEquivAlgOfEq.
- Defined in
- Mathlib.RingTheory.Ideal.Quotient.Defs
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RingHom.idproof · cited by 18,349
- Ringstatement and proof · cited by 7,463
- Idealstatement and proof · cited by 4,748
- LinearEquivproof · cited by 3,317
- HasQuotient.Quotientstatement and proof · cited by 2,301
- LinearEquiv.toLinearMapproof · cited by 1,171
- RingEquivstatement · cited by 1,147
- Ideal.IsTwoSidedstatement and proof · cited by 179
- AddHom.toFunproof · cited by 168
- LinearMap.toAddHomproof · cited by 165
- LinearEquiv.invFunproof · cited by 29
- Submodule.quotEquivOfEqproof · cited by 15
Cited by39
Results whose statement or proof uses this declaration.
- DoubleQuot.quotQuotEquivQuotOfLEproof · cited by 11
- RingEquiv.quotientBotproof · cited by 8
- Ideal.quotientMulEquivQuotientProdproof · cited by 8
- Int.quotientSpanNatEquivZModproof · cited by 7
- IsLocalization.AtPrime.equivQuotMaximalIdealproof · cited by 7
- DoubleQuot.quotQuotEquivCommproof · cited by 7
- AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuotproof · cited by 6
- AdjoinRoot.quotMapOfEquivQuotMapCMapMkproof · cited by 5
- KummerDedekind.quotMapEquivQuotQuotMapproof · cited by 5
- IsLocalization.AtPrime.equivQuotientMapOfIsMaximalproof · cited by 5
- Ideal.quotientInfEquivQuotientProdproof · cited by 5
- Int.quotientSpanEquivZModproof · cited by 4