flip_flip — Mathlib

English

For any bilinear map f, applying the flip operation twice returns the original map: f.flip.flip = f.

Русский

Для билинейного отображения f применение операции переворота два раза возвращает исходное отображение: f.flip.flip = f.

LaTeX

$$$ f.flip.flip = f $$$

Lean4

@[simp]
theorem flip_flip (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) : f.flip.flip = f :=
  LinearMap.ext₂ fun _x _y => (f.flip.flip_apply _ _).trans (f.flip_apply _ _)

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