Theorems · Theorem · commutative algebra

IsDedekindDomain.HeightOneSpectrum.equivPrimesOver.congr_simp

∀ {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),
  IsDedekindDomain.HeightOneSpectrum.equivPrimesOver B hp = IsDedekindDomain.HeightOneSpectrum.equivPrimesOver B hp

Defined in

Mathlib.RingTheory.DedekindDomain.Factorization

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIdeal.IsMaximalCommRingIsDedekindDomainAlgebraIsDomainModule.IsTorsionFree