English
A root-level version of the previous fact, deduced by rewriting via existing lemmas.
Русский
Корневая версия предыдущего факта, полученная извлеением через имеющиеся леммы.
LaTeX
$$Irreducible.normalizedFactors_pow {p} hp k := ...$$
Lean4
theorem normalizedFactors_prod_eq (s : Multiset α) (hs : ∀ a ∈ s, Irreducible a) :
normalizedFactors s.prod = s.map normalize := by
induction s using Multiset.induction with
| empty => rw [Multiset.prod_zero, normalizedFactors_one, Multiset.map_zero]
| cons a s ih =>
have ia := hs a (Multiset.mem_cons_self a _)
have ib := fun b h => hs b (Multiset.mem_cons_of_mem h)
obtain rfl | ⟨b, hb⟩ := s.empty_or_exists_mem
· rw [Multiset.cons_zero, Multiset.prod_singleton, Multiset.map_singleton, normalizedFactors_irreducible ia]
haveI := nontrivial_of_ne b 0 (ib b hb).ne_zero
rw [Multiset.prod_cons, Multiset.map_cons,
normalizedFactors_mul ia.ne_zero (Multiset.prod_ne_zero fun h => (ib 0 h).ne_zero rfl),
normalizedFactors_irreducible ia, ih ib, Multiset.singleton_add]
