sign_eq_sign_of_equiv — Mathlib

English

If two permutations f and g are related by a base equivalence e between their domains that commutes with the action, then they have the same sign.

Русский

Если две перестановки f и g связаны базовым эквивалентом e между их доменами и сохраняют действие, знаки совпадают.

LaTeX

$$$\\text{If } f:\\mathrm{Perm}(\\alpha),\\; g:\\mathrm{Perm}(\\beta),\\; e:\\alpha\\simeq\\beta,\\; \\forall x, e(f(x))=g(e(x)) \\Rightarrow \\operatorname{sign}(f)=\\operatorname{sign}(g)$$$

Lean4

theorem sign_eq_sign_of_equiv [DecidableEq β] [Fintype β] (f : Perm α) (g : Perm β) (e : α ≃ β)
    (h : ∀ x, e (f x) = g (e x)) : sign f = sign g :=
  by
  have hg : g = (e.symm.trans f).trans e := Equiv.ext <| by simp [h]
  rw [hg, sign_symm_trans_trans]

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