Theorems · Theorem · number theory

IsDedekindDomain.HeightOneSpectrum.intValuation_liesOver

∀ {A : Type u_1} {B : Type u_4} [inst : CommRing A] [inst_1 : IsDedekindDomain A] [inst_2 : CommRing B]
  [inst_3 : IsDedekindDomain B] [inst_4 : Algebra A B] [Module.IsTorsionFree A B]
  (v : IsDedekindDomain.HeightOneSpectrum A) (w : IsDedekindDomain.HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal]
  (x : A), v.intValuation x ^ v.asIdeal.ramificationIdx' w.asIdeal = w.intValuation ((algebraMap A B) x)

Defined in

Mathlib.NumberTheory.RamificationInertia.Valuation

Cited by

1 results in Mathlib

Foundations

Depth 154 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDedekindDomainCommRingIsDedekindDomainAlgebraModule.IsTorsionFreeIdeal.LiesOver