Zulip Chat Archive
Stream: mathlib4
Topic: Topology.ContinuousFunction.Basic
Moritz Doll (Feb 05 2023 at 11:58):
There are two errors left in !4#2053, if someone wants to have a look.
Kevin Buzzard (Feb 05 2023 at 14:11):
I've got one of them; I'll push when I've got both.
Kevin Buzzard (Feb 05 2023 at 14:24):
Got them. I added porting notes and pushed. It's unification being weaker?
Last updated: Dec 20 2023 at 11:08 UTC