flipLinear_flipMultilinear — Mathlib

English

The symmetric version of the flip multilinear equivalence matches the standard flipMultilinearEquiv under symm.

Русский

Симметричная версия эквивалентности переворота много-линейных отображений совпадает со стандартной flipMultilinearEquiv при симметрии.

LaTeX

$$$ ((flipMultilinearEquiv 𝕜 E G G').symm) = flipLinear $$$

Lean4

@[simp]
theorem flipLinear_flipMultilinear (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G') : f.flipMultilinear.flipLinear = f :=
  rfl

Похожие утверждения