Theorems · Theorem · functional analysis

ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_of_symmetric

∀ {𝕜 : 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 →L[𝕜] E →L[𝕜] E [⋀^Fin n]→L[𝕜] F},
  (∀ (x y : E), (f x) y = (f y) x) →
    ContinuousAlternatingMap.alternatizeUncurryFin (ContinuousAlternatingMap.alternatizeUncurryFinCLM 𝕜 E F ∘SL f) = 0

If f is a symmetric continuous bilinear map taking values in the space of continuous alternating maps, then the twice uncurried f is zero.

Defined in

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

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace