prod_normalizedFactors_eq — Mathlib

English

The product of normalizedFactors a equals normalize a (up to equality, since they are associated).

Русский

Произведение normalizedFactors a равно normalize a (с точностью до ассоциации).

LaTeX

$$normalizedFactors(a).prod = normalize(a)$$

Lean4

theorem prod_normalizedFactors_eq {a : α} (ane0 : a ≠ 0) : (normalizedFactors a).prod = normalize a :=
  by
  trans normalize (normalizedFactors a).prod
  · rw [normalizedFactors, ← map_multiset_prod, normalize_idem]
  · exact normalize_eq_normalize_iff.mpr (dvd_dvd_iff_associated.mpr (prod_normalizedFactors ane0))

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