prod_pow — Mathlib

English

For sets s ⊆ α and t ⊆ β, the nth power of the product set equals the product of nth powers: (s ×ˢ t)^n = (s^n) ×ˢ (t^n) for all n.

Русский

Для множеств s ⊆ α и t ⊆ β выполняется (s ×ˢ t)^n = (s^n) ×ˢ (t^n) для всех n.

LaTeX

$$$\forall s \subseteq \alpha, \forall t \subseteq \beta, \forall n, (s \timesˢ t)^n = (s^n) \timesˢ (t^n)$$$

Lean4

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

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