Proof of continuous_bilinear

[Louis-Le-Grand]

Proof of continuous_bilinear under the conditions that the modules A M and A N are free and finite. For this we added:

• def LinearMap.smul₁ /.smul₂ the definition of left and right scalar multiplication
• instance Module.instContinuousSMul show scalar multiplicationis Continuous
• def LinearMap.prodfst /.prodsnd the definition of the projection of the product space on its components
• instance Module.instCommAdd show addition is commutative
• def LinearMap.basis₁ representation of object by there basis
• lemma continuous_bilinear

[kbuzzard]

I didn't read the first big proof yet; I was hoping that it somehow wouldn't be necessary, but maybe it is. The issue seems to be that you want to consider two topologies on A even though they're the same :-/

[kbuzzard]

This is looking great now! Well done! Tidy up any final bits, deal with the comments and I'll merge.

[kbuzzard]

We definitely don't want definitions which are already there, hopefully you can use what we have.

[kbuzzard]

One last thing: I am beginning to understand now that some results are true without assuming commutativity. Perhaps you should have a Ring section of the file where all the theorems that work fine without commutativity are proved in the correct generality, and then a CommRing section where the proofs which need commutativity go. So you'd have variables in each section, or you have some convention that all commutative top rings are called A and all noncommutative ones are called B or whatever.

[kbuzzard]

Thanks a lot!