prod_smul — Mathlib

English

For any natural d and a prime multiset u, the product of d • u equals the product of u raised to the power d.

Русский

Для любого натурального d и мультимножества простых u, произведение d • u равно произведению u в степени d.

LaTeX

$$$ (d \\cdot u).prod = u.prod^{\\,d} $$$

Lean4

theorem prod_smul (d : ℕ) (u : PrimeMultiset) : (d • u).prod = u.prod ^ d := by
  induction d with
  | zero => simp only [zero_nsmul, pow_zero, prod_zero]
  | succ n ih => rw [succ_nsmul, prod_add, ih, pow_succ]

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