Module

IsRegularLocalRing_uniqueFactorizationMonoid_of_ringKrullDim_le_two.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsRegularLocalRing_uniqueFactorizationMonoid_of_ringKrullDim_le_two

3 declarations indexed from sourceView source ↗

Module documentation

Is Regular Local Ring unique Factorization Monoid of ring Krull Dim le two

Imports4

Imported by1

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.All

theorem

isPrincipalIdealRing_of_spanFinrank_eq_one

L31 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_uniqueFactorizationMonoid_of_ringKrullDim_le_two.AB2UFD.isPrincipalIdealRing_of_spanFinrank_eq_one

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_uniqueFactorizationMonoid_of_ringKrullDim_le_two
open IsLocalRing
namespace AB2UFD

Lean source · statement

theorem isPrincipalIdealRing_of_spanFinrank_eq_one (S : Type*) [CommRing S] [IsRegularLocalRing S]
    (h : Submodule.spanFinrank (maximalIdeal S) = 1) : IsPrincipalIdealRing S

theorem

isPrincipalIdealRing_of_maximalIdeal_eq_bot

L40 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_uniqueFactorizationMonoid_of_ringKrullDim_le_two.AB2UFD.isPrincipalIdealRing_of_maximalIdeal_eq_bot

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_uniqueFactorizationMonoid_of_ringKrullDim_le_two
open IsLocalRing
namespace AB2UFD

Lean source · statement

theorem isPrincipalIdealRing_of_maximalIdeal_eq_bot (S : Type*) [CommRing S] [IsLocalRing S]
    (h : maximalIdeal S = ⊥) : IsPrincipalIdealRing S

theorem

uniqueFactorizationMonoid_of_ringKrullDim_le_two

L51 ↗

IsRegularLocalRing.uniqueFactorizationMonoid_of_ringKrullDim_le_two

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_uniqueFactorizationMonoid_of_ringKrullDim_le_two
open IsLocalRing
open AB2UFD in

Lean source · statement

theorem _root_.IsRegularLocalRing.uniqueFactorizationMonoid_of_ringKrullDim_le_two
    (R : Type*) [CommRing R] [IsRegularLocalRing R] [IsDomain R] (hdim : ringKrullDim R ≤ 2) :
    UniqueFactorizationMonoid R

Module documentation

Is Regular Local Ring unique Factorization Monoid of ring Krull Dim le two

Declarations

isPrincipalIdealRing_of_spanFinrank_eq_one

isPrincipalIdealRing_of_maximalIdeal_eq_bot

uniqueFactorizationMonoid_of_ringKrullDim_le_two