Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-15 13:39 2395183b

View on Github →

feat(analysis/topology/quotient_topological_structures): endow quotient of topological groups, add groups and rings with a topological whatever structure This is not yet sorted. I'd like to push completions before cleaning this.

Estimated changes