normalizedFactors_of_irreducible_pow

English

If p is irreducible in α, then the normalized factors of p^k are exactly k copies of the normalization of p.

Русский

Если p ирредуцируем в α, то нормализованные факторы p^k состоят ровно из k копий нормализации p.

LaTeX

$$normalizedFactors(p^k) = \operatorname{Multiset}.replicate(k, \operatorname{normalize}(p))$$

Lean4

theorem normalizedFactors_of_irreducible_pow {p : α} (hp : Irreducible p) (k : ℕ) :
    normalizedFactors (p ^ k) = Multiset.replicate k (normalize p) := by
  rw [normalizedFactors_pow, normalizedFactors_irreducible hp, Multiset.nsmul_singleton]

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