MIL bump

Stream: general

[Kim Morrison]

https://github.com/avigad/mathematics_in_lean_source/pull/217

[Patrick Massot]

Thanks!

[Patrick Massot]

What is happening with μ.ae vs ae μ?

[Kim Morrison]

Not sure. Looks like a PR from Yury ~2 months ago, that didn't install a deprecation.

[Patrick Massot]

I see, this is generalizing the input of ae. I guess this isn’t a bit issue since it appears only in the context of saying there is a special notation for Filter.eventually in this case.

[Patrick Massot]

The Nat.card mess is much worse.

[Notification Bot]

6 messages were moved here from #general > Cannot get Lean4 and Mathlib working in Emacs by Patrick Massot.

[Patrick Massot]

Do we have a better story to tell than: Mathlib randomly uses Fintype.card and Nat.card?

[Yaël Dillies]

I had the story that Mathlib uses Fintype.card except when it can't, but now I don't know :sad:

[Patrick Massot]

This is really a nightmare. Half of the lemmas use one and half use the other. And I am talking only about lemmas about cardinals of subgroups.

[Michael Rothgang]

If I understand correctly, there's a pending migration from Fintype.card to Nat.card; #14789 is the most recent PR. CC @Thomas Browning

[Thomas Browning]

At least for groups, Nat.card is definitely preferable. Most theorems in group theory about cardinalities are purely multiplicative statements (e.g., $\lvert H\rvert\cdot\lvert G/H\rvert=\lvert G\rvert$) so they generalize to infinite groups (e.g., #13431). This also connects nicely with orders of elements, where the kernel of $\mathbb{Z}\to\langle g\rangle$ has kernel generated by orderOf g, even when g has infinite order.

The group theory library has been a messy mix of both, but I've been slowly switching things over (sometimes with impressive results: #13637!). Most of the churn should be over. I think the only low-level file left is OrderOfElement.lean.

[Kim Morrison]

Unfortunately these refactors are hard to do atomically, and this MIL bump is badly timed. I think merging the current state but revisiting in a few weeks (or when Thomas says it's a good time!) will eventually reach a good result.

[Patrick Massot]

It’s already great to learn that things are moving and there is hope.

[Patrick Massot]

Do we have a Nat.card version of docs#Fintype.card_eq_one_iff ?

[Patrick Massot]

Same for docs#Fintype.bijective_iff_injective_and_card

[Peter Nelson]

Not as single lemmas, but you can potentially use docs#Set.ncard_univ and the ncard API to help with things like that.

[Patrick Massot]

In the mean time I opened #107568 #14825

[Peter Nelson]

Wrong PR link there : #14825

[Patrick Massot]

Thanks. I wonder where I took the wrong number…

[Patrick Massot]

@Peter Nelson I updated the PR with the refinement you wanted.

[Patrick Massot]

Note the above PR was merged by Kim so I have been able to bump Mathlib in MIL to use those new lemmas. So there is no longer any use of Fintype.card in that MIL file.