Module

IsLocalRing_two_le_ringKrullDim_adicCompletion_of_two_le.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_two_le_ringKrullDim_adicCompletion_of_two_le

1 declaration indexed from sourceView source ↗

Module documentation

Is Local Ring two le ring Krull Dim adic Completion of two le

Imports3

Mathlib.RingTheory.KrullDimension.Basic
Mathlib.RingTheory.Ideal.GoingDown
Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_faithfullyFlat_adicCompletion_maximalIdeal

Imported by1

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.All

theorem

two_le_ringKrullDim_adicCompletion_of_two_le

L28 ↗

IsLocalRing.two_le_ringKrullDim_adicCompletion_of_two_le

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_two_le_ringKrullDim_adicCompletion_of_two_le

Lean source · statement

theorem _root_.IsLocalRing.two_le_ringKrullDim_adicCompletion_of_two_le
    (R : Type*) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] (h : 2 ≤ ringKrullDim R) :
    2 ≤ ringKrullDim (AdicCompletion (IsLocalRing.maximalIdeal R) R)

Module documentation

Is Local Ring two le ring Krull Dim adic Completion of two le

Declarations

two_le_ringKrullDim_adicCompletion_of_two_le