English
If D is a UFD, then the multivariate polynomial ring MvPolynomial σ D is a UFD as well.
Русский
Если D — UFD, то полиномы MvPolynomial σ D также образуют UFD.
LaTeX
$$$$\\text{If } D \\text{ is a UFD, then } \\operatorname{MvPolynomial}_{\\sigma} (D) \\text{ is a UFD}. $$$$
Lean4
instance (priority := 100) uniqueFactorizationMonoid : UniqueFactorizationMonoid (MvPolynomial σ D) :=
by
rw [iff_exists_prime_factors]
intro a ha; obtain ⟨s, a', rfl⟩ := exists_finset_rename a
obtain ⟨w, h, u, hw⟩ :=
iff_exists_prime_factors.1 (uniqueFactorizationMonoid_of_fintype s) a' fun h => ha <| by simp [h]
exact
⟨w.map (rename (↑)), fun b hb =>
let ⟨b', hb', he⟩ := Multiset.mem_map.1 hb
he ▸ (prime_rename_iff (σ := σ) ↑s).2 (h b' hb'),
Units.map (@rename s σ D _ (↑)).toRingHom.toMonoidHom u, by
rw [Multiset.prod_hom, Units.coe_map, AlgHom.toRingHom_eq_coe, RingHom.toMonoidHom_eq_coe,
AlgHom.toRingHom_toMonoidHom, MonoidHom.coe_coe, ← map_mul, hw]⟩
