Commit 2021-02-19 07:04 a0e2b3c4

View on Github →

chore(topology/Profinite): reduce universe variables (#6300) See https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/universe.20issue

Estimated changes