Julien Puydt (Jun 22 2022 at 09:47): Julien Puydt (Jun 22 2022 at 09:47):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: Apr 20 2024 at 02:40 UTC