Theorems · Theorem · functional analysis

OrthonormalBasis.det_to_matrix_orthonormalBasis_of_same_orientation

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2} [inst_2 : Fintype ι]
  [inst_3 : DecidableEq ι] (e f : OrthonormalBasis ι ℝ E),
  e.toBasis.orientation = f.toBasis.orientation → e.toBasis.det ⇑f = 1

The change-of-basis matrix between two orthonormal bases with the same orientation has determinant 1.

Defined in: Mathlib.Analysis.InnerProductSpace.Orientation
Cited by: 1 results in Mathlib
Foundations: Depth 233 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup InnerProductSpace Fintype DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites17

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Realstatement and proof · cited by 25,697
NormedAddCommGroupstatement and proof · cited by 15,752
Fintypestatement and proof · cited by 7,736
InnerProductSpacestatement and proof · cited by 3,523
Nat.cast_oneproof · cited by 2,501
Nat.cast_zeroproof · cited by 1,870
Orientationstatement · cited by 360
AlternatingMapstatement · cited by 329
neg_neg_of_posproof · cited by 227
OrthonormalBasisstatement and proof · cited by 188
sub_eq_zero_of_eqproof · cited by 154

Cited by1

Results whose statement or proof uses this declaration.

OrthonormalBasis.same_orientation_iff_det_eq_detproof · cited by 1