Theorems · Theorem · group theory

Equiv.Perm.sign_subtypeCongr

∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] {p : α → Prop} [inst_2 : DecidablePred p]
  (ep : Equiv.Perm { a // p a }) (en : Equiv.Perm { a // ¬p a }),
  Equiv.Perm.sign (ep.subtypeCongr en) = Equiv.Perm.sign ep * Equiv.Perm.sign en

Defined in

Mathlib.GroupTheory.Perm.Sign

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeDecidablePred