normalizedFactors_pow — Mathlib

English

For any finite multiset s of irreducibles, normalizedFactors s.prod equals s.map normalize.

Русский

Для конечного множества s нерaзложимых элементов, нормализованные факторы s.prod равны s.map normalize.

LaTeX

$$normalizedFactors(s.prod) = s.map normalize$$

Lean4

@[simp]
theorem normalizedFactors_pow {x : α} (n : ℕ) : normalizedFactors (x ^ n) = n • normalizedFactors x := by
  induction n with
  | zero => simp [zero_nsmul]
  | succ n ih =>
    by_cases h0 : x = 0
    · simp [h0, zero_pow n.succ_ne_zero, nsmul_zero]
    rw [pow_succ', succ_nsmul', normalizedFactors_mul h0 (pow_ne_zero _ h0), ih]

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