star_prod — Mathlib

English

Star distributes over finite products: star of a finite product equals the product of stars.

Русский

Звезда распределяется по конечным произведениям: star над произведением равно произведению звёзд.

LaTeX

$$$\star\left( \prod_{x\in s} f(x) \right) = \prod_{x\in s} \star( f(x) ).$$$

Lean4

@[simp]
theorem star_prod [CommMonoid R] [StarMul R] {α : Type*} (s : Finset α) (f : α → R) :
    star (∏ x ∈ s, f x) = ∏ x ∈ s, star (f x) :=
  map_prod (starMulAut : R ≃* R) _ _

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