Module

ringKrullDim_le_of_ringHom_isIntegral.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.ringKrullDim_le_of_ringHom_isIntegral

1 declaration indexed from sourceView source ↗

Module documentation

ring Krull Dim le of ring Hom is Integral

Imports3

Mathlib.RingTheory.Spectrum.Prime.RingHom
Mathlib.RingTheory.Ideal.GoingUp
Mathlib.RingTheory.KrullDimension.Basic

Imported by1

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.All

theorem

ringKrullDim_le_of_ringHom_isIntegral

L29 ↗

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace ringKrullDim_le_of_ringHom_isIntegral
universe u v

Lean source · statement

theorem _root_.ringKrullDim_le_of_ringHom_isIntegral
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] (φ : R →+* S) (hφ : φ.IsIntegral) :
    ringKrullDim S ≤ ringKrullDim R

Module documentation

ring Krull Dim le of ring Hom is Integral

Declarations

ringKrullDim_le_of_ringHom_isIntegral