Theorems · Definition · commutative algebra
RingEquiv.quotientBot
(R : Type u_1) → [inst : Ring R] → R ⧸ ⊥ ≃+* R
The quotient of a ring by he zero ideal is isomorphic to the ring itself.
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Ring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ringstatement and proof · cited by 7,463
- Idealstatement · cited by 4,748
- Bot.botstatement · cited by 4,720
- HasQuotient.Quotientstatement · cited by 2,301
- RingEquivstatement · cited by 1,147
- RingEquiv.transproof · cited by 54
- Ideal.quotEquivOfEqproof · cited by 15
- RingHom.quotientKerEquivOfRightInverseproof · cited by 3
Cited by9
Results whose statement or proof uses this declaration.
- AlgEquiv.quotientBotproof · cited by 5
- Module.supportDim_self_eq_ringKrullDimproof · cited by 3
- PrimeSpectrum.mem_image_comap_basicOpenproof · cited by 3
- NumberField.InfinitePlace.inertiaDeg_eq_finrankproof · cited by 2
- Ideal.inertiaDeg'_botproof · cited by 1
- AlgebraicGeometry.isIso_of_comp_eq_sigmaSpecproof · cited by 1
- IsArtinianRing.finite_of_compactSpace_of_t2Spaceproof · cited by 0
- RingEquiv.quotientBot_mkstatement · cited by 0
- RingEquiv.quotientBot_symm_mkstatement · cited by 0