finsupp_single — Mathlib

English

For g ∈ G and a ∈ A, applying ρ.finsupp α to the single basis element δ_x with value δ_x a yields δ_x applied to ρ(g) a, i.e., (ρ.finsupp α g)(single x a) = single x (ρ(g) a).

Русский

Для данного g и a, применение ρ.finsupp α к базисному элементу δ_x даёт δ_x, применяющее ρ(g) к a; т.е. (ρ.finsupp α g)(single x a) = single x (ρ(g) a).

LaTeX

$$$ ρ.finsupp α g (single x a) = single x (ρ g a) $$$

Lean4

@[simp]
theorem finsupp_single (g : G) (x : α) (a : A) : ρ.finsupp α g (single x a) = single x (ρ g a) := by
  simp [finsupp_apply]

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