Theorems · Theorem · linear algebra

AlternatingMap.neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq

∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ} (f : M [⋀^Fin n]→ₗ[R] N) {v : Fin (n + 1) → M}
  {i j : Fin (n + 1)}, v i = v j → i ≠ j → (-1) ^ ↑i • f (i.removeNth v) + (-1) ^ ↑j • f (j.removeNth v) = 0

Let v be an (n + 1)-tuple with two equal elements v i = v j, i ≠ j. Let w i (resp., w j) be the vector v with ith (resp., jth) element removed. Then (-1) ^ i • f (w i) + (-1) ^ j • f (w j) = 0. This follows from the fact that these two vectors differ by a permutation of sign (-1) ^ (i + j). These are the only two nonzero terms in the proof of map_eq_zero_of_eq in the definition of alternatizeUncurryFin below.

Defined in

Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupAddCommGroupModuleModule