Continuous algebra equivalences

[kbuzzard]

We don't have ContinuousAlgEquiv in mathlib as far as I can see: this is the structure whose terms are continuous R-algebra isomorphisms with continuous inverses. We do have ContinuousLinearEquiv though, so it's just a case of putting together this and AlgEquiv.

The reason we need it: we want to state that if L/K is a finite extension of number fields and v is a finite place of K, then the algebra isomorphism L tensor_K K_v = prod_{w|v} L_w is bicontinuous.

[grunweg]

claim

[grunweg]

(My current plan is to get to this "somewhen this week". If this is more urgent, let me know and I can prioritise this, or disclaim the task.)

[smmercuri]

I'm just seeing this now, I have an API for ContinuousAlgEquiv in my repo that I worked on last week. I can PR it!

[grunweg]

Sure, that sounds good - I'll be happy to review.