theorem PowerSeriesUFD.maximalIdeal_eq_span_X' (k : Type u_1) [Field k] : IsLocalRing.maximalIdeal (PowerSeries k) = Ideal.span {PowerSeries.X}

The maximal ideal of k[[x]] is the principal ideal (x).

instance PowerSeriesUFD.mvPowerSeries_fin_isDomain (k : Type u_1) [Field k] (n : ℕ) : IsDomain (MvPowerSeries (Fin n) k)

The power series ring k[[x_1,...,x_n]] is an integral domain.

instance PowerSeriesUFD.mvPowerSeries_fin_isLocalRing (k : Type u_1) [Field k] (n : ℕ) : IsLocalRing (MvPowerSeries (Fin n) k)

The power series ring k[[x_1,...,x_n]] is a local ring.

theorem PowerSeriesUFD.regularLocalRing_isUFD (R : Type u_2) [CommRing R] [IsRegularLocalRing R] [IsDomain R] : UniqueFactorizationMonoid R

Auslander-Buchsbaum theorem: every regular local ring is a UFD.

theorem PowerSeriesUFD.mvPowerSeries_isRegularLocalRing (k : Type u_1) [Field k] (n : ℕ) : IsRegularLocalRing (MvPowerSeries (Fin n) k)

The power series ring k[[x_1,...,x_n]] is a regular local ring.

instance PowerSeriesUFD.mvPowerSeries_isUFD (k : Type u_1) [Field k] (n : ℕ) : UniqueFactorizationMonoid (MvPowerSeries (Fin n) k)

The power series ring k[[x_1,...,x_n]] is a UFD (Proposition 23, Lecture 15).

theorem PowerSeriesUFD.ufd_of_completion_ufd (A : Type u_2) [CommRing A] [IsDomain A] [IsLocalRing A] [IsNoetherianRing A] (hcompl : UniqueFactorizationMonoid (AdicCompletion (IsLocalRing.maximalIdeal A) A)) : UniqueFactorizationMonoid A

Descent: a Noetherian local domain whose completion is a UFD is itself a UFD (Proposition 23, Lecture 15).