norm_ofDistribMulAction_eq — Mathlib

English

For a finite group G acting on A by DistribMulAction, the norm map equals the sum over G of the action: norm x = ∑_{g∈G} g • x.

Русский

Для конечной группы G действующей на A через DistribMulAction норма равна сумме действий: norm x = ∑_{g∈G} g • x.

LaTeX

$$$\\operatorname{norm}(x) = \\sum_{g \\in G} g \\cdot x$$$

Lean4

@[simp]
theorem norm_ofDistribMulAction_eq {G : Type*} [Group G] [Fintype G] [DistribMulAction G A] [SMulCommClass G k A]
    (x : A) : (ofDistribMulAction k G A).norm x = ∑ g : G, g • x := by simp [norm]

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