Theorems · Theorem · commutative algebra

IsDedekindDomain.HeightOneSpectrum.equivPrimesOver_apply

∀ {A : Type u_4} [inst : CommRing A] {p : Ideal A} [hpm : p.IsMaximal] (B : Type u_5) [inst_1 : CommRing B]
  [inst_2 : IsDedekindDomain B] [inst_3 : Algebra A B] [inst_4 : IsDomain A] [inst_5 : Module.IsTorsionFree A B]
  (hp : p ≠ 0) (v : { v // v.asIdeal ∣ Ideal.map (algebraMap A B) p }),
  ↑((IsDedekindDomain.HeightOneSpectrum.equivPrimesOver B hp) v) = (↑v).asIdeal

Defined in

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIdeal.IsMaximalCommRingIsDedekindDomainAlgebraIsDomainModule.IsTorsionFree