continuousMultilinearMapCongrLeft_symm

English

The equality of the coe of the symm-flip equivalence is the same as the flip of the linear map.

Русский

Сравнение переходов через симметричную эквивалентность и flip совпадает с flip LinearMap.

LaTeX

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

Lean4

@[simp]
theorem _root_.ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_symm (f : ∀ i, E i ≃L[𝕜] E₁ i) :
    (ContinuousLinearEquiv.continuousMultilinearMapCongrLeft G f).symm =
      .continuousMultilinearMapCongrLeft G fun i : ι => (f i).symm :=
  rfl

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