Theorems · Theorem · functional analysis

ContinuousAlternatingMap.neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq

∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ} (f : E [⋀^Fin n]→L[𝕜] F)
  {v : Fin (n + 1) → E} {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 AlternatingMap.alternatizeUncurryFin.

Defined in

Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace