Theorems · Definition · commutative algebra

IsDedekindDomainDvr.casesOn

{A : Type u_1} →
  [inst : CommRing A] →
    [inst_1 : IsDomain A] →
      {motive : IsDedekindDomainDvr A → Sort u} →
        (t : IsDedekindDomainDvr A) →
          ([toIsNoetherian : IsNoetherian A A] →
              (is_dvr_at_nonzero_prime :
                  ∀ (P : Ideal A), P ≠ ⊥ → ∀ (x : P.IsPrime), IsDiscreteValuationRing (Localization.AtPrime P)) →
                motive ⋯) →
            motive t

Defined in

Mathlib.RingTheory.DedekindDomain.Dvr

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsDomain