smul_prod_perm — Mathlib

English

For a finite group G acting on N, the product over all h ∈ G of (h • b) is fixed by any g ∈ G: g • ∏_{h∈G} (h • b) = ∏_{h∈G} (h • b).

Русский

При конечной группе G, действующей на N, произведение по всем h∈G (h•b) стабильно при любом g∈G: g•(...)=....

LaTeX

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

Lean4

theorem smul_prod_perm [Fintype G] (b : N) (g : G) : (g • ∏ h : G, h • b) = ∏ h : G, h • b :=
  by
  simp only [smul_prod', smul_smul]
  exact Finset.prod_bijective (g * ·) (Group.mulLeft_bijective g) (by simp) (fun _ _ ↦ rfl)

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