Theorems · Definition · group theory

Equiv.Perm.signAux3

{α : Type u} → [DecidableEq α] → [Finite α] → Equiv.Perm α → {s : Multiset α} → (∀ (x : α), x ∈ s) → ℤˣ

When the multiset s : Multiset α contains all nonfixed points of the permutation f : Perm α, signAux2 f _ recursively calculates the sign of f.

Defined in

Mathlib.GroupTheory.Perm.Sign

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEqFinite