associated_of_factorization_eq — Mathlib

English

If a,b ≠ 0 and factorization(a) = factorization(b), then a and b are associated.

Русский

Если a,b ≠ 0 и factorization(a) = factorization(b), то a и b ассоциированы.

LaTeX

$$$a \\neq 0,\\ b \\neq 0,\\ \\text{factorization}(a) = \\text{factorization}(b) \\Rightarrow a \\sim b$$$

Lean4

theorem associated_of_factorization_eq (a b : α) (ha : a ≠ 0) (hb : b ≠ 0) (h : factorization a = factorization b) :
    Associated a b := by
  simp_rw [factorization, AddEquiv.apply_eq_iff_eq] at h
  rwa [associated_iff_normalizedFactors_eq_normalizedFactors ha hb]

Похожие утверждения