primeFactors_val_eq_normalizedFactors

English

If a is radical, then the underlying multiset of prime factors of a equals the multiset of normalized factors of a.

Русский

Для радикального элемента a множество простых факторов a, рассматриваемое как мультисет, совпадает с мультисетом нормализованных факторов a.

LaTeX

$$$ IsRadical(a) \Rightarrow (\operatorname{primeFactors}(a)).\mathrm{val} = \operatorname{normalizedFactors}(a) $$$

Lean4

theorem primeFactors_val_eq_normalizedFactors (ha : IsRadical a) : (primeFactors a).val = normalizedFactors a := by
  classical
  rw [primeFactors, Multiset.toFinset_val, Multiset.dedup_eq_self]
  exact normalizedFactors_nodup ha

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