(* Title: Three_Squares/Low_Dimensional_Linear_Algebra.thy Author: Anton Danilkin *) section ‹Vectors and matrices, determinants and their properties in dimensions 2 and 3› theory Low_Dimensional_Linear_Algebra imports "HOL-Library.Adhoc_Overloading" begin