Interaction entre algèbre linéaire et analyse en formalisation des mathématiques. (Interaction between linear algebra and analysis in formal mathematics). - Guillaume Cano (2014)

Formalized linear algebra over Elementary Divisor Rings in Coq. - Guillaume Cano; Cyril Cohen; Maxime Dénès; Anders Mörtberg; Vincent Siles (Log. Methods Comput. Sci., 2016)