Formalization of complex analysis and matrix theory

DOI10.1007/978-981-15-7261-6MaRDI QIDQ5119159zbMATH OpenOpenAlexFDO

Authors Zhiping Shi, Yong Guan, Ximeng Li

Publication date 3 September 2020

Full work available at URL https://doi.org/10.1007/978-981-15-7261-6

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to linear algebra (15-02) Research exposition (monographs, survey articles) pertaining to functions of a complex variable (30-02) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Formalization of function matrix theory in HOL
• Formalization of functional variation in HOL Light
• Formalization of transform methods using HOL Light
• Formalization of complex vectors in higher-order logic
• On the formalization of Fourier transform in higher-order logic

Cited in

(5)

• Formalization of function matrix theory in HOL
• Formalization of operations of block matrix based on Coq
• Formalism, Hamilton and complex numbers
• scientific article; zbMATH DE number 1907864 (Why is no real title available?)
• Formalization of complex vectors in higher-order logic

Describes a project that uses

Uses Software

• Isabelle/HOL
• Mizar
• PVS
• HOL
• HOL Light
• Flyspeck

This page was built for publication: Formalization of complex analysis and matrix theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5119159)