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
chore(topology/Profinite): reduce universe variables (#6300) See https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/universe.20issue