mathlib3
a0e2b3c4 - chore(topology/Profinite): reduce universe variables (#6300)

Commit
4 years ago
chore(topology/Profinite): reduce universe variables (#6300) See https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/universe.20issue Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading