mulOpposite — Mathlib

English

The multiplicative opposite of an orthonormal basis b is an orthonormal basis for the opposite space Hᵐᵒᵖ.

Русский

У ортонормированной базы b, её умноженная противоположная версия образует ортонормированную базу для пространства MulOpposite.

LaTeX

$$OrthonormalBasis.mulOpposite 𝕜 H$$

Lean4

/-- The multiplicative opposite of an orthonormal basis `b`, i.e., `b i ↦ op (b i)`. -/
noncomputable def _root_.OrthonormalBasis.mulOpposite {ι : Type*} [Fintype ι] (b : OrthonormalBasis ι 𝕜 H) :
    OrthonormalBasis ι 𝕜 Hᵐᵒᵖ :=
  b.toBasis.mulOpposite.toOrthonormalBasis b.orthonormal

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