NYLL
Module

isRegularLocalRing_localization_atPrime_mvPolynomial.lean

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

Module documentation

is Regular Local Ring localization at Prime mv Polynomial

Imports1
  • Mathlib.RingTheory.RegularLocalRing.Polynomial
Imported by2

Declarations

theorem

isRegularLocalRing_localization_atPrime_mvPolynomial

L24 ↗
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace isRegularLocalRing_localization_atPrime_mvPolynomial
Lean source · statement
theorem _root_.isRegularLocalRing_localization_atPrime_mvPolynomial (k : Type*) [Field k] (n : ℕ)
  (q : Ideal (MvPolynomial (Fin n) k)) [q.IsPrime] :
    IsRegularLocalRing (Localization.AtPrime q)

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