[Merged by Bors] - feat(Topology/Group): continuous isomorphism#16991
[Merged by Bors] - feat(Topology/Group): continuous isomorphism#16991Thmoas-Guan wants to merge 82 commits intomasterfrom
Conversation
PR summary 4656ab5736Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
and use correct notation in def
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
|
I'm happy with this now -- @urkud are you? |
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
…r-community/mathlib4 into continuous-isomorphism
Define the continuous isomorphisms of multiplicative and additive topological group.
|
Pull request successfully merged into master. Build succeeded! And happy new year! 🎉 |
Define the continuous isomorphisms of multiplicative and additive topological group.