IsLocalRing.faithfullyFlat_adicCompletion_maximalIdeal
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_faithfullyFlat_adicCompletion_maximalIdeal
open IsLocalRingLean source · statement
theorem _root_.IsLocalRing.faithfullyFlat_adicCompletion_maximalIdeal (R : Type*) [CommRing R]
[IsNoetherianRing R] [IsLocalRing R] :
Module.FaithfullyFlat R (AdicCompletion (IsLocalRing.maximalIdeal R) R)