Mathlib Map

Theorems · Theorem · commutative algebra

IsDedekindDomain.HeightOneSpectrum.emultiplicity_iSup

∀ {R : Type u_3} [inst : CommRing R] [IsDedekindDomain R] (p : IsDedekindDomain.HeightOneSpectrum R) {ι : Type u_4}
  [Finite ι] (I : ι → Ideal R), emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i)
Defined in
Mathlib.RingTheory.DedekindDomain.Factorization
Cited by
1 results in Mathlib
Foundations
Depth 155 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommRingIsDedekindDomainFinite
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsDedekindDomain.HeightOneSpectrum.multiplicity_iSup · cited by 0HeightOneSpectrum.multipl…DFunLike.coe · cited by 62936DFunLike.coeSet · cited by 53352SetCommRing · cited by 17173CommRingEquiv · cited by 8337EquivFintype · cited by 7736FintypeENat · cited by 4985ENatIdeal · cited by 4748IdealBot.bot · cited by 4720Bot.botSet.range · cited by 4705Set.rangeFinite · cited by 3029FiniteiSup · cited by 2415iSupiInf · cited by 1690iInfSupSet.sSup · cited by 954SupSet.sSupInfSet.sInf · cited by 935InfSet.sInfIsDedekindDomain · cited by 668IsDedekindDomainHeightOneSpectrum.emultiplici…CITED BYCITES

Cites28

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

  • DFunLike.coeproof · cited by 62,936
  • Setproof · cited by 53,352
  • CommRingstatement and proof · cited by 17,173
  • Equivproof · cited by 8,337
  • Fintypeproof · cited by 7,736
  • ENatstatement and proof · cited by 4,985
  • Idealstatement and proof · cited by 4,748
  • Bot.botproof · cited by 4,720
  • Set.rangeproof · cited by 4,705
  • Finitestatement and proof · cited by 3,029
  • iSupstatement and proof · cited by 2,415
  • iInfstatement and proof · cited by 1,690

Cited by1

Results whose statement or proof uses this declaration.