Commit 2024-04-24 08:44 51ee7399
View on Github →feat(Inseparable): Prod.map mk mk is a quotient map (#12327)
This is needed to prove continuity of binary arithmetic operations
on the separation quotient.
feat(Inseparable): Prod.map mk mk is a quotient map (#12327)
This is needed to prove continuity of binary arithmetic operations
on the separation quotient.