product_pow — Mathlib

English

In a product monoid, the nth power distributes over Finset product: (s ×ˢ t)^n = (s^n) ×ˢ (t^n).

Русский

В произведении моноидов: (s ×ˢ t)^n = (s^n) ×ˢ (t^n).

LaTeX

$$$(s \times^{\mathrm{Finset}} t)^n = (s^n) \times^{\mathrm{Finset}} (t^n)$$$

Lean4

@[to_additive]
theorem product_pow [Monoid β] (s : Finset α) (t : Finset β) : ∀ n, (s ×ˢ t) ^ n = (s ^ n) ×ˢ (t ^ n)
  | 0 => by simp
  | n + 1 => by simp [pow_succ, product_pow _ _ n]

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