Theorems · Theorem · group theory

Equiv.Perm.signAux3_symm_trans_trans

∀ {α : Type u} [inst : DecidableEq α] {β : Type v} [inst_1 : Finite α] [inst_2 : DecidableEq β] [inst_3 : Finite β]
  (f : Equiv.Perm α) (e : α ≃ β) {s : Multiset α} {t : Multiset β} (hs : ∀ (x : α), x ∈ s) (ht : ∀ (x : β), x ∈ t),
  Equiv.Perm.signAux3 ((e.symm.trans f).trans e) ht = f.signAux3 hs

Defined in: Mathlib.GroupTheory.Perm.Sign
Cited by: 1 results in Mathlib
Foundations: Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DecidableEq Finite DecidableEq Finite

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Equivstatement and proof · cited by 8,337
Equiv.symmstatement and proof · cited by 3,681
Finitestatement and proof · cited by 3,029
Unitsstatement and proof · cited by 2,804
Multisetstatement and proof · cited by 2,627
Equiv.Permstatement and proof · cited by 1,375
Equiv.transstatement and proof · cited by 337
Finite.exists_equiv_finproof · cited by 23
Equiv.Perm.signAuxproof · cited by 8
Equiv.Perm.signAux2proof · cited by 5
Equiv.Perm.signAux3statement · cited by 2

Cited by1

Results whose statement or proof uses this declaration.

Equiv.Perm.sign_symm_trans_transproof · cited by 2