Theorems · Theorem · commutative algebra
Ideal.Quotient.nontrivial_iff
∀ {R : Type u_3} [inst : Ring R] {I : Ideal R}, Nontrivial (R ⧸ I) ↔ I ≠ ⊤- Defined in
- Mathlib.RingTheory.Ideal.Quotient.Basic
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 71 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.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Top.topstatement · cited by 9,680
- Ringstatement and proof · cited by 7,463
- Idealstatement and proof · cited by 4,748
- Nontrivialstatement · cited by 2,416
- HasQuotient.Quotientstatement · cited by 2,301
- Submodule.Quotient.nontrivial_iffproof · cited by 13
Cited by9
Results whose statement or proof uses this declaration.
- ringKrullDim_quotient_succ_le_of_nonZeroDivisorproof · cited by 3
- PowerSeries.IsWeierstrassFactorizationAt.map_ne_zero_of_ne_topproof · cited by 3
- Polynomial.Monic.exists_splits_mapproof · cited by 2
- IsLocalRing.exists_maximalIdeal_pow_le_of_isArtinianRing_quotientproof · cited by 2
- Ideal.Quotient.nontrivial_of_liesOver_of_ne_topproof · cited by 1
- Ideal.FinrankQuotientMap.span_eq_topproof · cited by 1
- exists_integral_inj_algHom_of_quotientproof · cited by 1
- isJacobsonRing_of_isIntegralproof · cited by 1
- Algebra.FormallyUnramified.isField_quotient_map_maximalIdealproof · cited by 1