Theorems · Theorem · group theory

Equiv.Perm.prod_Iio_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) → ∏ j, ∏ i < j, f (σ i) (σ j) = ↑↑(Equiv.Perm.sign σ) * ∏ j, ∏ i < j, f i j

Defined in

Mathlib.GroupTheory.Perm.Fin

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRing