Theorems · Theorem · group theory

Equiv.Perm.prod_Ioi_comp_eq_sign_mul_prod

∀ {n : ℕ} {R : Type u_1} [inst : CommRing R] (σ : Equiv.Perm (Fin n)) {f : Fin n → Fin n → R},
  (∀ (i j : Fin n), f i j = -f j i) → ∏ i, ∏ j > i, f (σ i) (σ j) = ↑↑(Equiv.Perm.sign σ) * ∏ i, ∏ j > i, f i j

Defined in

Mathlib.GroupTheory.Perm.Fin

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRing