Theorem gramSchmidtOrthonormalBasis_det

Modification history

2023-06-02 11:07

Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean

feat: port Analysis.InnerProductSpace.Orientation (#4503)

Modified gramSchmidtOrthonormalBasis_det View on Github →

2023-05-30 07:01

Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean

feat: port Analysis.InnerProductSpace.GramSchmidtOrtho (#4473)

Added gramSchmidtOrthonormalBasis_det View on Github →