Theorems · Theorem · commutative algebra

primesOver_finite

Deprecated since 2026-04-16Use IsDedekindDomain.primesOver_finite instead.

∀ {A : Type u_4} [inst : CommRing A] (p : Ideal A) [hpm : p.IsMaximal] (B : Type u_5) [inst_1 : CommRing B]
  [IsDedekindDomain B] [inst_3 : Algebra A B] [IsDomain A] [Module.IsTorsionFree A B] [Algebra.IsIntegral A B],
  (p.primesOver B).Finite

Alias of IsDedekindDomain.primesOver_finite.

Defined in: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Cited by: 0 results in Mathlib
Foundations: Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing Ideal.IsMaximal CommRing IsDedekindDomain Algebra IsDomain Module.IsTorsionFree Algebra.IsIntegral

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites11

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

CommRingstatement · cited by 17,173
Algebrastatement · cited by 11,388
Idealstatement · cited by 4,748
IsDomainstatement · cited by 2,196
Set.Finitestatement · cited by 1,814
IsDedekindDomainstatement · cited by 668
Module.IsTorsionFreestatement · cited by 600
Ideal.IsMaximalstatement · cited by 452
Algebra.IsIntegralstatement · cited by 224
Ideal.primesOverstatement · cited by 84
IsDedekindDomain.primesOver_finiteproof · cited by 2

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.