Theorems · Theorem · group theory

Equiv.Perm.sign_trans_trans

∀ {α : Type u} [inst : DecidableEq α] {β : Type v} [inst_1 : Fintype α] [inst_2 : DecidableEq β] [inst_3 : Fintype β]
  (f : β ≃ α) (p : Equiv.Perm α) (g : α ≃ β),
  Equiv.Perm.sign (f.trans (Equiv.trans p g)) = Equiv.Perm.sign p * Equiv.Perm.sign (f.trans g)

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

DecidableEqFintypeDecidableEqFintype