Theorems · Theorem · commutative algebra

IsLocalRing.primesOverFinset_eq

∀ {R : Type u_1} [inst : CommRing R] (A : Type u_4) [inst_1 : CommRing A] [IsDomain A] [inst_3 : IsLocalRing A]
  [inst_4 : IsDedekindDomain A] [inst_5 : Algebra R A] [FaithfulSMul R A] [Module.Finite R A] {p : Ideal R}
  [p.IsMaximal], p ≠ ⊥ → IsDedekindDomain.primesOverFinset p A = {IsLocalRing.maximalIdeal A}

Defined in: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Cited by: 1 results in Mathlib
Foundations: Depth 152 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing CommRing IsDomain IsLocalRing IsDedekindDomain Algebra FaithfulSMul Module.Finite Ideal.IsMaximal

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites18

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

Setproof · cited by 53,352
CommRingstatement and proof · cited by 17,173
Finsetstatement · cited by 13,712
Algebrastatement and proof · cited by 11,388
Idealstatement and proof · cited by 4,748
Bot.botstatement and proof · cited by 4,720
IsDomainstatement and proof · cited by 2,196
Module.Finitestatement and proof · cited by 1,032
IsDedekindDomainstatement and proof · cited by 668
Ideal.IsMaximalstatement and proof · cited by 452
FaithfulSMulstatement and proof · cited by 340
IsLocalRingstatement and proof · cited by 339

Cited by1

Results whose statement or proof uses this declaration.

Ideal.ramificationIdx_mul_inertiaDeg_of_isLocalRingproof · cited by 0