map_perm — Mathlib

English

The map g evaluated at a permuted argument equals the original value multiplied by the sign of the permutation.

Русский

Значение g на переставленных аргументах равно исходному значению, умноженному на знаковость перестановки.

LaTeX

$$g (v ∘ σ) = sign(σ) • g v$$

Lean4

theorem map_perm [DecidableEq ι] [Fintype ι] (v : ι → M) (σ : Equiv.Perm ι) : g (v ∘ σ) = Equiv.Perm.sign σ • g v := by
  induction σ using Equiv.Perm.swap_induction_on' with
  | one => simp
  | mul_swap s x y hxy hI => simp_all [← Function.comp_assoc, g.map_swap]

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