dualBasis_flip_dualBasis — Mathlib

English

The dual basis constructed from the flip of B, applied to the dual basis of B, returns the original basis: B.flip.dualBasis hB.flip (B.dualBasis hB b) = b.

Русский

База двойственной базы, построенная по перевернутой форме B, примененная к двойственной базе B возвращает исходную базу: B.flip.dualBasis hB.flip (B.dualBasis hB b) = b.

LaTeX

$$$B.flip.dualBasis(hB.flip, B.dualBasis(hB,b)) = b$$$

Lean4

@[simp]
theorem dualBasis_flip_dualBasis (B : BilinForm K V) (hB : B.Nondegenerate) {ι} [Finite ι] [DecidableEq ι]
    [FiniteDimensional K V] (b : Basis ι K V) : B.flip.dualBasis hB.flip (B.dualBasis hB b) = b :=
  dualBasis_dualBasis_flip _ hB.flip b

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