Module

IsLocalRing_uniqueFactorizationMonoid_of_isPrincipalIdealRing_quotient.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_uniqueFactorizationMonoid_of_isPrincipalIdealRing_quotient

1 declaration indexed from sourceView source ↗

Module documentation

Is Local Ring unique Factorization Monoid of is Principal Ideal Ring quotient

Imports6

Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Mathlib.RingTheory.Nakayama
Mathlib.RingTheory.Noetherian.Defs
Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain
Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
Mathlib.Tactic.Ring.RingNF

Imported by2

theorem

uniqueFactorizationMonoid_of_isPrincipalIdealRing_quotient

L29 ↗

IsLocalRing.uniqueFactorizationMonoid_of_isPrincipalIdealRing_quotient

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_uniqueFactorizationMonoid_of_isPrincipalIdealRing_quotient

Lean source · statement

theorem _root_.IsLocalRing.uniqueFactorizationMonoid_of_isPrincipalIdealRing_quotient
    {A : Type*} [CommRing A] [IsDomain A] [IsNoetherianRing A] [IsLocalRing A] (t : A)
    [IsDomain (A ⧸ Ideal.span {t})] [IsPrincipalIdealRing (A ⧸ Ideal.span {t})] :
    UniqueFactorizationMonoid A

Module documentation

Is Local Ring unique Factorization Monoid of is Principal Ideal Ring quotient

Declarations

uniqueFactorizationMonoid_of_isPrincipalIdealRing_quotient