Theorems · Theorem · commutative algebra

IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {r : R},
  r ≠ 0 →
    v.intValuationDef r = WithZero.exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors))

Defined in: Mathlib.RingTheory.DedekindDomain.AdicValuation
Cited by: 3 results in Mathlib
Foundations: Depth 149 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing IsDedekindDomain

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites14

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

Setstatement · cited by 53,352
CommRingstatement and proof · cited by 17,173
Idealstatement · cited by 4,748
Ideal.spanstatement · cited by 948
Multiplicativestatement · cited by 875
IsDedekindDomainstatement and proof · cited by 668
WithZerostatement · cited by 586
IsDedekindDomain.HeightOneSpectrumstatement and proof · cited by 338
IsDedekindDomain.HeightOneSpectrum.asIdealstatement · cited by 156
Associates.mkstatement · cited by 137
WithZero.expstatement · cited by 112
Associates.factorsstatement · cited by 97

Cited by3

Results whose statement or proof uses this declaration.

IsDedekindDomain.HeightOneSpectrum.intValuation_if_negproof · cited by 11
IsDedekindDomain.HeightOneSpectrum.intValuation.map_add_le_max'proof · cited by 0
IsDedekindDomain.HeightOneSpectrum.intValuation.map_one'proof · cited by 0