search

sudgy / math-from-nothing

Developing mathematics in Coq from the ground up
GNU Lesser General Public License v2.1
17 stars 1 forks source link

Deal with repeated proofs in Linear Algebra #7

Open sudgy opened 2 years ago

sudgy commented 2 years ago

As it currently stands, there are several repeated proofs about the idea of dealing with unique representations of elements in a linear space. They should all be redone to use GradedSpace in some way, which should be able to handle any of those issues. Some particularly egregious offenders are bases and the free space.

sudgy commented 2 years ago

This also involves trying to find a better way to deal with spaces constructed as the infinite direct sum of other spaces