English
If x ≠ 0 and y ≠ 0, then normalizedFactors(x*y) = normalizedFactors x + normalizedFactors y.
Русский
Если x ≠ 0 и y ≠ 0, то normalizedFactors(xy) = normalizedFactors x + normalizedFactors y.
LaTeX
$$normalizedFactors(x*y) = normalizedFactors(x) + normalizedFactors(y)$$
Lean4
@[simp]
theorem normalizedFactors_mul {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :
normalizedFactors (x * y) = normalizedFactors x + normalizedFactors y :=
by
have h : (normalize : α → α) = Associates.out ∘ Associates.mk :=
by
ext
rw [Function.comp_apply, Associates.out_mk]
rw [← Multiset.map_id' (normalizedFactors (x * y)), ← Multiset.map_id' (normalizedFactors x), ←
Multiset.map_id' (normalizedFactors y), ← Multiset.map_congr rfl normalize_normalized_factor, ←
Multiset.map_congr rfl normalize_normalized_factor, ← Multiset.map_congr rfl normalize_normalized_factor, ←
Multiset.map_add, h, ← Multiset.map_map Associates.out, eq_comm, ← Multiset.map_map Associates.out]
refine congr rfl ?_
apply Multiset.map_mk_eq_map_mk_of_rel
apply factors_unique
· intro x hx
rcases Multiset.mem_add.1 hx with (hx | hx) <;> exact irreducible_of_normalized_factor x hx
· exact irreducible_of_normalized_factor
· rw [Multiset.prod_add]
exact
((prod_normalizedFactors hx).mul_mul (prod_normalizedFactors hy)).trans
(prod_normalizedFactors (mul_ne_zero hx hy)).symm
