prod_normalizedFactors — Mathlib

English

For any nonzero a, the product of normalizedFactors a is associated to a.

Русский

Произведение нормализованных факторов a ассоциировано с a, если a ≠ 0.

LaTeX

$$Associated((normalizedFactors(a)).prod, a)$$

Lean4

theorem prod_normalizedFactors {a : α} (ane0 : a ≠ 0) : Associated (normalizedFactors a).prod a :=
  by
  rw [normalizedFactors, factors, dif_neg ane0]
  refine Associated.trans ?_ (Classical.choose_spec (exists_prime_factors a ane0)).2
  rw [← Associates.mk_eq_mk_iff_associated, ← Associates.prod_mk, ← Associates.prod_mk, Multiset.map_map]
  congr 2
  ext
  rw [Function.comp_apply, Associates.mk_normalize]

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