optionCongr_sign — Mathlib

English

The parity/sign of a permutation is preserved when extended to Option α by optionCongr, assuming α is finite.

Русский

Знак перестановки сохраняется при расширении до Option α через optionCongr при условии конечности α.

LaTeX

$$$ \\mathrm{Perm.sign}(e.\\mathrm{optionCongr}) = \\mathrm{Perm.sign}(e) $$$

Lean4

@[simp]
theorem optionCongr_sign {α : Type*} [DecidableEq α] [Fintype α] (e : Perm α) : Perm.sign e.optionCongr = Perm.sign e :=
  by
  induction e using Perm.swap_induction_on with
  | one => simp [Perm.one_def]
  | swap_mul f x y hne h => simp [h, hne, Perm.mul_def]

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