Formalization of Fabry-Perot Resonator in HOL Light


Technical Report


Linear algebra is a mathematical theory which is essential to both pure and applied mathematics. While many theorem provers support linear spaces, they usually consider only real vector spaces or provide very abstract formalizations which are useful for the formalization of mathematics but lack many notions required for applied mathematics and therefore many other fields, e.g., computer science, engineering, physics, economics, natural sciences, etc. In this paper, we propose a new formalization of complex linear algebras whose objective is to be a toolbox for various engineering applications.


Concordia University