NYLL
Module

IsLocalRing_ringKrullDim_adicCompletion_maximalIdeal_eq.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_ringKrullDim_adicCompletion_maximalIdeal_eq
1 declaration indexed from sourceView source ↗

Module documentation

Is Local Ring ring Krull Dim adic Completion maximal Ideal eq

Imports7
Imported by1

Declarations

theorem

ringKrullDim_adicCompletion_maximalIdeal_eq

L32 ↗
IsLocalRing.ringKrullDim_adicCompletion_maximalIdeal_eq
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_ringKrullDim_adicCompletion_maximalIdeal_eq
open IsLocalRing in
Lean source · statement
theorem _root_.IsLocalRing.ringKrullDim_adicCompletion_maximalIdeal_eq
    (R : Type*) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] :
    ringKrullDim (AdicCompletion (IsLocalRing.maximalIdeal R) R) = ringKrullDim R

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