For my students, all linear algebra is over a field, and only the real field or the complex field are allowed. Granted, most exercises/results only need any field. A large chunk of the rest depend on it being infinite, and some just specify completely the field, so the question is partially moot.

But still, this is a valid and simple mathematical situation I don't know how coq can handle: assume $\mathbb K\in\{\mathbb R, \mathbb C\}$... then work with vector spaces and linear maps over this field. That means it has to be a field. And if the fact that it's infinite is needed (so that a polynomial with too many roots is in fact zero, generally), that should come pretty easily.

Last updated: Sep 26 2023 at 13:01 UTC