mathlib documentation


Orientations of real inner product spaces. #

This file provides definitions and proves lemmas about orientations of real inner product spaces.

Main definitions #

basis.adjust_to_orientation, applied to an orthonormal basis, produces an orthonormal basis.

noncomputable def orientation.fin_orthonormal_basis {E : Type u_1} [inner_product_space E] {n : } (hn : 0 < n) (h : finite_dimensional.finrank E = n) (x : orientation E (fin n)) :
basis (fin n) E

An orthonormal basis, indexed by fin n, with the given orientation.


orientation.fin_orthonormal_basis gives a basis with the required orientation.