Theorems · Theorem · functional analysis

OrthonormalBasis.det_to_matrix_orthonormalBasis_real

∀ {ι : Type u_1} {F : Type u_5} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] [inst_2 : Fintype ι]
  [inst_3 : DecidableEq ι] (a b : OrthonormalBasis ι ℝ F), a.toBasis.det ⇑b = 1 ∨ a.toBasis.det ⇑b = -1

The determinant of the change-of-basis matrix between two orthonormal bases a, b is ±1.

Defined in

Mathlib.Analysis.InnerProductSpace.PiL2

Cited by

2 results in Mathlib

Foundations

Depth 232 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceFintypeDecidableEq