Module

isRegularLocalRing_localization_atPrime_of_etale_of_comap.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.isRegularLocalRing_localization_atPrime_of_etale_of_comap

2 declarations indexed from sourceView source ↗

Module documentation

is Regular Local Ring localization at Prime of etale of comap

Imports5

Mathlib.RingTheory.Etale.Basic
Mathlib.RingTheory.Flat.Localization
Mathlib.RingTheory.RegularLocalRing.Defs
Mathlib.RingTheory.Smooth.Flat
Mathlib.RingTheory.Unramified.LocalRing

Imported by2

theorem

isNoetherianRing_of_essFiniteType

L34 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.isRegularLocalRing_localization_atPrime_of_etale_of_comap.ChildB.isNoetherianRing_of_essFiniteType

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace isRegularLocalRing_localization_atPrime_of_etale_of_comap
noncomputable section
open IsLocalRing Localization
namespace ChildB

Lean source · statement

theorem isNoetherianRing_of_essFiniteType (R S : Type*) [CommRing R] [CommRing S]
    [Algebra R S] [IsNoetherianRing R] [Algebra.EssFiniteType R S] :
    IsNoetherianRing S

theorem

isRegularLocalRing_localization_atPrime_of_etale_of_comap

L43 ↗

Source context 5 commands