English
For compatible isomorphisms, applying the inverse equivalence to a factor gives the corresponding factor after taking equivalence into account.
Русский
При совместимых изоморфизмах применение симметричного эквивалента к фактору возвращает соответствующий фактор после учёта эквивалентности.
LaTeX
$$normalizedFactorsEquiv_symm_apply (he) {a} {q} (hq) : (normalizedFactorsEquiv he a).symm ⟨q, hq⟩ = (MulEquivClass.toMulEquiv f).symm q$$
Lean4
theorem normalizedFactors_multiset_prod (s : Multiset α) (hs : 0 ∉ s) :
normalizedFactors (s.prod) = (s.map normalizedFactors).sum :=
by
cases subsingleton_or_nontrivial α
· obtain rfl : s = 0 := by
apply Multiset.eq_zero_of_forall_notMem
intro _
convert hs
simp
induction s using Multiset.induction with
| empty => simp
| cons _ _ IH =>
rw [Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons, normalizedFactors_mul, IH]
· exact fun h ↦ hs (Multiset.mem_cons_of_mem h)
· exact fun h ↦ hs (h ▸ Multiset.mem_cons_self _ _)
· apply Multiset.prod_ne_zero
exact fun h ↦ hs (Multiset.mem_cons_of_mem h)
