WIP Classification theorem for GL0

[TBUGTB]

No description provided.

[kbuzzard]

I think that you should not be launching into a proof of bijectivity. In type theory this is an unnatural statement. You should inhabit the equiv instead, and probably comment out the aux lemma. You are basically doing the thing below the lemma, but within a proof, and what you're doing is sufficiently useful that it needs to be a standalone thing.

[TBUGTB]

Thanks for the comment, I switched to proving an instance of Equiv. I also separated out the definition of a (constant) automorphic form because it's become quite long.

[kbuzzard]

Thanks a lot! There seems to be some other stuff here too (in a totally different file), possibly I accidentally pushed to your branch after reviewing. Sorry! Your work looks fine :-)