leanprover-community / lean-perfectoid-spaces

Perfectoid spaces in the Lean formal theorem prover.
https://leanprover-community.github.io/lean-perfectoid-spaces/
Apache License 2.0
115 stars 13 forks source link

Main lemma to continuously extend multiplication #11

Closed PatrickMassot closed 6 years ago

PatrickMassot commented 6 years ago

This should be most of the hard work needed to get a multiplication map on the completion of a topological ring. This is Bourbaki GT III.6.5 Theorem I: ℤ-bilinear continuous maps from dense sub-groups into a complete Hausdorff group extend by continuity. Note that Bourbaki assumes that E and F are also complete Hausdorff, but this is a typo.