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

The formal power series ring k[[x_1, ..., x_n]] over a field is a domain.

theorem auslander_buchsbaum_UFD (R : Type u_2) [CommRing R] [IsRegularLocalRing R] [IsDomain R] : UniqueFactorizationMonoid R

Auslander–Buchsbaum: every regular local ring (which is a domain) is a UFD.

theorem mvPowerSeries_fin_isRegularLocalRing (k : Type u_1) [Field k] (n : ℕ) : IsRegularLocalRing (MvPowerSeries (Fin n) k)

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

theorem prop23_power_series_UFD (k : Type u_1) [Field k] (n : ℕ) : UniqueFactorizationMonoid (MvPowerSeries (Fin n) k)

Proposition 23 (a): the formal power series ring k[[x_1, ..., x_n]] over a field is a UFD.

theorem prop23_UFD_of_completion_UFD (A : Type u_2) [CommRing A] [IsDomain A] [IsLocalRing A] [IsNoetherianRing A] (hUFD : UniqueFactorizationMonoid (AdicCompletion (IsLocalRing.maximalIdeal A) A)) : UniqueFactorizationMonoid A

Proposition 23 (b): if a Noetherian local domain A has UFD completion, then A itself is a UFD.