English
An integral domain with a unit times irreducible factorization property has a well-defined irreducible factorization up to associates.
Русский
Целостный делитель с единицей имеет разложение на ирредуцируемые элементы безразлично к ассоциированию.
LaTeX
$$$\forall p,q\, Irreducible p, Irreducible q → Associated p q$$$
Lean4
theorem unique_irreducible (hR : HasUnitMulPowIrreducibleFactorization R) ⦃p q : R⦄ (hp : Irreducible p)
(hq : Irreducible q) : Associated p q := by
rcases hR with ⟨ϖ, hϖ, hR⟩
suffices ∀ {p : R} (_ : Irreducible p), Associated p ϖ by apply Associated.trans (this hp) (this hq).symm
clear hp hq p q
intro p hp
obtain ⟨n, hn⟩ := hR hp.ne_zero
have : Irreducible (ϖ ^ n) := hn.symm.irreducible hp
rcases lt_trichotomy n 1 with (H | rfl | H)
· obtain rfl : n = 0 := by
clear hn this
revert H n
decide
simp [not_irreducible_one, pow_zero] at this
· simpa only [pow_one] using hn.symm
· obtain ⟨n, rfl⟩ : ∃ k, n = 1 + k + 1 := Nat.exists_eq_add_of_lt H
rw [pow_succ'] at this
rcases this.isUnit_or_isUnit rfl with (H0 | H0)
· exact (hϖ.not_isUnit H0).elim
· rw [add_comm, pow_succ'] at H0
exact (hϖ.not_isUnit (isUnit_of_mul_isUnit_left H0)).elim
