smul_finprod_perm — Mathlib

English

For a finite group G acting on N, the same invariance holds for finprod: (g • ∏ᶠ h∈G, h • b) = ∏ᶠ h∈G, h • b.

Русский

Для конечной группы G действует на N; аналогично для финпроизводства: g•(финпроизвод) = финпроизвод.

LaTeX

$$$\\forall {N} [\\mathsf{CommMonoid} N] {G} [\\mathsf{Group} G] (b:N) (g:G),\\; g \\cdot \\mathrm{finprod}\\ h: G, h \\cdot b = \\mathrm{finprod}\\ h: G, h \\cdot b$$$

Lean4

theorem smul_finprod_perm [Finite G] (b : N) (g : G) : (g • ∏ᶠ h : G, h • b) = ∏ᶠ h : G, h • b :=
  by
  cases nonempty_fintype G
  simp only [finprod_eq_prod_of_fintype, Finset.smul_prod_perm]

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