dualBasis_dualBasis_flip — Mathlib

English

Let B be nondegenerate. Then B.flip is nondegenerate as well; swapping the arguments preserves nondegeneracy.

Русский

Пусть B невырождена. Тогда B.flip также невырождена; поменяв аргументы, сохраняется невырожденность.

LaTeX

$$$\\operatorname{Nondegenerate}(B) \\implies \\operatorname{Nondegenerate}(B^{\\mathrm{flip}}).$$$

Lean4

@[simp]
theorem dualBasis_dualBasis_flip [FiniteDimensional K V] (B : BilinForm K V) (hB : B.Nondegenerate) {ι : Type*}
    [Finite ι] [DecidableEq ι] (b : Basis ι K V) : B.dualBasis hB (B.flip.dualBasis hB.flip b) = b :=
  by
  ext i
  refine LinearMap.ker_eq_bot.mp hB.ker_eq_bot ((B.flip.dualBasis hB.flip b).ext (fun j ↦ ?_))
  simp_rw [apply_dualBasis_left, ← B.flip_apply, apply_dualBasis_left, @eq_comm _ i j]

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