factors_pow — Mathlib

English

For any x and natural n, the factors of x^n are associated to n copies of the factors of x.

Русский

Разложение x^n связано с повторением разложения x n раз.

LaTeX

$$$\forall x\in \alpha, n\in \mathbb{N},\; \mathrm{factors}(x^n) \sim Associated\; n\cdot \mathrm{factors}(x).$$$

Lean4

theorem factors_pow {x : α} (n : ℕ) : Multiset.Rel Associated (factors (x ^ n)) (n • factors x) := by
  match n with
  | 0 => rw [zero_nsmul, pow_zero, factors_one, Multiset.rel_zero_right]
  | n + 1 =>
    by_cases h0 : x = 0
    · simp [h0, zero_pow n.succ_ne_zero, nsmul_zero]
    · rw [pow_succ', succ_nsmul']
      refine Multiset.Rel.trans _ (factors_mul h0 (pow_ne_zero n h0)) ?_
      refine Multiset.Rel.add ?_ <| factors_pow n
      exact Multiset.rel_refl_of_refl_on fun y _ => Associated.refl _

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