Mathlib Map

Theorems · Theorem · commutative algebra

Ideal.span_singleton_eq_bot

∀ {α : Type u} [inst : Semiring α] {x : α}, Ideal.span {x} = ⊥ ↔ x = 0
Defined in
Mathlib.RingTheory.Ideal.Span
Cited by
27 results in Mathlib
Foundations
Depth 27 from the axioms · uses propext, Quot.sound
Assumes
Semiring
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

FractionalIdeal.count_well_defined · cited by 5FractionalIdeal.count_wel…FractionalIdeal.count_mul · cited by 4FractionalIdeal.count_mulAssociates.mk_ne_zero' · cited by 4Associates.mk_ne_zero'IsDiscreteValuationRing.irreducible_iff_uniformizer · cited by 4IsDiscreteValuationRing.i…FractionalIdeal.constant_factor_ne_zero · cited by 3FractionalIdeal.constant_…IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd · cited by 3HeightOneSpectrum.intValu…Ideal.eq_span_singleton_of_height_eq_one · cited by 2Ideal.eq_span_singleton_o…Ring.isField_iff_maximal_bot · cited by 2Ring.isField_iff_maximal_…FractionalIdeal.not_inv_le_one_of_ne_bot · cited by 2FractionalIdeal.not_inv_l…Ring.HasFiniteQuotients.finite_setOfPred_mem · cited by 2HasFiniteQuotients.finite…UniqueFactorizationMonoid.of_forall_isPrincipal_of_height_eq_one · cited by 1UniqueFactorizationMonoid…maximalIdeal_isPrincipal_of_isDedekindDomain · cited by 1maximalIdeal_isPrincipal_…associated_norm_prod_smith · cited by 1associated_norm_prod_smithNumberField.not_dvd_discr_iff_isUnramifiedIn · cited by 1NumberField.not_dvd_discr…finrank_quotient_span_eq_natDegree_norm · cited by 1finrank_quotient_span_eq_…Set · cited by 53352SetSemiring · cited by 13802SemiringIdeal · cited by 4748IdealBot.bot · cited by 4720Bot.botIdeal.span · cited by 948Ideal.spanIdeal.span_singleton_eq_botCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement · cited by 53,352
  • Semiringstatement and proof · cited by 13,802
  • Idealstatement · cited by 4,748
  • Bot.botstatement · cited by 4,720
  • Ideal.spanstatement · cited by 948

Cited by27

Results whose statement or proof uses this declaration.