mathlib

mathlib copied to clipboard

We enforce a canonical way to compare cardinals a and b of different universes u and v, namely to compare cardinal.lift.{v} a and cardinal.lift.{u} b. By doing this, we alleviate some of the universe hell going on with cardinal.lift.

We rename basis.mk_eq_dim'' to basis.mk_eq_dim', since the latter name was used for a non-complying theorem that has been purged.

---

LGTM but let's wait for one more pair of eyes: I don't want to make decisions about universe-related questions by myself.

Thanks! By the way, should I add a library note explaining the changes here?

Yes.

Sorry this has taken a long time. I am skeptical about the loss of generality, but if you can convince someone who know about the cardinal library I'm not going to object.

In the meantime, there are now merge conflicts with master. If you'd still like to proceed with this, can you please merge master?

The recent renaming of vector space dimension theorems caused some annoying merge conflicts, but they seem to be fixed now.

The recent renaming of vector space dimension theorems caused some annoying merge conflicts, but they seem to be fixed now.

Apologies, my ongoing dimension refactor has created a few more conflicts, hopefully minor.

CI is failing

CI passes now. If we want this before the mathlib4 port of the vector space files it's probably best to merge this before any other major changes to these files.

maintainer merge

🚀 Pull request has been placed on the maintainer queue by alreadydone.

I think per https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/New.20policy.20regarding.20mathlib3.20PRs.20that.20touch.20ported.20files this can't be merged for now, unless there is some reason this is needed for porting to proceed.