Theorems · Theorem · group theory

Equiv.Perm.sign_subtypePerm

∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α) {p : α → Prop} [inst_2 : DecidablePred p]
  (h₁ : ∀ (x : α), p (f x) ↔ p x), (∀ (x : α), f x ≠ x → p x) → Equiv.Perm.sign (f.subtypePerm h₁) = Equiv.Perm.sign f

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