NYLL
Module

IsLocalRing_exists_dvd_pow_of_krullDimLE_one.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_exists_dvd_pow_of_krullDimLE_one
2 declarations indexed from sourceView source ↗

Module documentation

Is Local Ring exists dvd pow of krull Dim LE one

Imports2
  • Mathlib.RingTheory.KrullDimension.Basic
  • Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Imported by1

Declarations

theorem

exists_dvd_pow

L29 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_exists_dvd_pow_of_krullDimLE_one.RankOneNilSol.exists_dvd_pow
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_exists_dvd_pow_of_krullDimLE_one
open IsLocalRing
namespace RankOneNilSol
Lean source · statement
theorem exists_dvd_pow {R : Type*} [CommRing R] [IsDomain R] [IsLocalRing R] [Ring.KrullDimLE 1 R]
    {b : R} (hb : b ≠ 0) {c : R} (hc : c ∈ maximalIdeal R) : ∃ n : ℕ, b ∣ c ^ n
theorem

exists_dvd_pow_of_krullDimLE_one

L50 ↗
IsLocalRing.exists_dvd_pow_of_krullDimLE_one
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_exists_dvd_pow_of_krullDimLE_one
open IsLocalRing
Lean source · statement
theorem _root_.IsLocalRing.exists_dvd_pow_of_krullDimLE_one
    {R : Type*} [CommRing R] [IsDomain R] [IsLocalRing R] [Ring.KrullDimLE 1 R]
    {b : R} (hb : b ≠ 0) {c : R} (hc : c ∈ IsLocalRing.maximalIdeal R) : ∃ n : ℕ, b ∣ c ^ n

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