On the formalization of Gram-Schmidt process for orthonormalizing a set of vectors
From MaRDI portal
Publication:6071622
DOI10.2478/forma-2023-0005OpenAlexW4387107320MaRDI QIDQ6071622
Publication date: 28 November 2023
Published in: Formalized Mathematics (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2478/forma-2023-0005
Application of orthogonal and other special functions (94A11) Orthogonalization in numerical linear algebra (65F25) Formalization of mathematics in connection with theorem provers (68V20) Linear algebra (educational aspects) (97H60)
Cites Work
- Unnamed Item
- Unnamed Item
- The role of the Mizar mathematical library for interactive proof development in Mizar
- Real vector space and related notions
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- Algebraic Numbers in Isabelle/HOL
- Mizar: State-of-the-art and Beyond
This page was built for publication: On the formalization of Gram-Schmidt process for orthonormalizing a set of vectors
