NYLL
Module

ValuationSubring_finite_primeSpectrum_of_ringKrullDim_lt_top.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_finite_primeSpectrum_of_ringKrullDim_lt_top
2 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring finite prime Spectrum of ring Krull Dim lt top

Imports5
  • Mathlib.RingTheory.Valuation.ValuationSubring
  • Mathlib.RingTheory.KrullDimension.Basic
  • Mathlib.Order.KrullDimension
  • Mathlib.Data.Finset.Sort
  • Mathlib.Data.Fintype.EquivFin
Imported by1

Declarations

lemma

finite_of_krullDim_lt_top

L32 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_finite_primeSpectrum_of_ringKrullDim_lt_top.AbhFinSol.finite_of_krullDim_lt_top
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finite_primeSpectrum_of_ringKrullDim_lt_top
namespace AbhFinSol
open ValuationSubring
Lean source · statement
lemma finite_of_krullDim_lt_top (P : Type*) [LinearOrder P] (h : Order.krullDim P < ⊤) :
    Finite P
theorem

finite_primeSpectrum_of_ringKrullDim_lt_top

L53 ↗
ValuationSubring.finite_primeSpectrum_of_ringKrullDim_lt_top
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finite_primeSpectrum_of_ringKrullDim_lt_top
open AbhFinSol in
Lean source · statement
theorem _root_.ValuationSubring.finite_primeSpectrum_of_ringKrullDim_lt_top {L : Type*} [Field L]
  (A : ValuationSubring L) (h : ringKrullDim A < ⊤) :
    Finite (PrimeSpectrum A)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.