Theorems · Theorem · group theory

Equiv.Perm.sign_bij

∀ {α : Type u} [inst : DecidableEq α] {β : Type v} [inst_1 : Fintype α] [inst_2 : DecidableEq β] [inst_3 : Fintype β]
  {f : Equiv.Perm α} {g : Equiv.Perm β} (i : (x : α) → f x ≠ x → β),
  (∀ (x : α) (hx : f x ≠ x) (hx' : f (f x) ≠ f x), i (f x) hx' = g (i x hx)) →
    (∀ (x₁ x₂ : α) (hx₁ : f x₁ ≠ x₁) (hx₂ : f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂) →
      (∀ (y : β), g y ≠ y → ∃ x, ∃ (hx : f x ≠ x), i x hx = y) → Equiv.Perm.sign f = Equiv.Perm.sign g

Defined in

Mathlib.GroupTheory.Perm.Sign

Cited by

1 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintypeDecidableEqFintype