Mathlib PRs

Stream: FLT-regular

[Andrew Yang]

#8464 moves multiset-relating lemmas by Ruben

[Ruben Van de Velde]

And #8486 for UFDs

[Riccardo Brasca]

I will have a look at this tomorrow if it still open.

[Riccardo Brasca]

BTW @Chris Birkbeck we have a red X on github about "build documentation". Is this the blueprint?

[Chris Birkbeck]

Hmm yeah it is. The blueprint still seems to be working, but I will have a look and see if I can figure out what the problem is.

[Andrew Yang]

I might have removed the proof of 5.1 in that PR. This might be the problem?

[Chris Birkbeck]

I don't see why that would be a problem, but who knows.

[Ruben Van de Velde]

Does the blueprint verify that the lean statements you link to actually exist?

[Chris Birkbeck]

Good question. I used to not do that, but maybe now with the doc-gen thing it does.

[Chris Birkbeck]

I can't quite figure out what the problem is. I tried undoing the change to the blueprint, but it didn't work. Maybe @Utensil Song can spot what the problem is? It seems to be breaking while building the documentation see here

[Mauricio Collares]

You need to bump the doc-gen4 dependency (just running lake update and committing the manifest changes should be enough)

[Mauricio Collares]

This was fixed in leanprover/doc-gen4#164 (yes, there are "fix: " commits there too)

[Chris Birkbeck]

Ok great, I'll try that, thank you!

[Chris Birkbeck]

hmm ok now it failed further along. During the copy documentation step, saying mv: cannot stat 'build/doc': No such file or directory.

[Mauricio Collares]

I guess build/doc is now .lake/build/doc

[Mauricio Collares]

(in push.yml)

[Chris Birkbeck]

oh ok, let me try that now :)

[Riccardo Brasca]

It worked, thanks!

[Chris Birkbeck]

oh great! thank you!

[Yaël Dillies]

If you need any help with your blueprint, I'm here as well.

[Andrew Yang]

List of currently open Mathlib PRs:
#8625 (delegated)
#8639 (needs fix)
#8641
#8645
#8651
#8653
#8654
#8657

[Riccardo Brasca]

I've left a couple of comments.

[Ruben Van de Velde]

I'll push a bump in a few minutes

[Andrew Yang]

There are several PRs moving results into mathlib. It would be great if someone could review them so that we may bump the mathlib version and do some clean up before lean together.
#9412: Rank-nullity for commutative integral domains (does not contain the potentially controversial bits)
#9397: Criterion for $X^n - a$ to be irreducible for odd $n$.
#9368: Cyclic extensions are of the form $K[\sqrt[n]{a}]$.
#9293: Defines the class IsUnramifiedAtInfinitePlaces.
#9265: Define intNorm and intTrace.
And also #9444 which adds four more instances but slows down the whole mathlib by ~10%.

[Kevin Buzzard]

@Eric Wieser do you trust the output of bench in #9444 ?

[Eric Wieser]

I think there's something wonky with tactic execution, I saw a similar jump in one of my PRs

[Eric Wieser]

I believe the other two bench outputs

[Riccardo Brasca]

I will surely have time next week if those are still open

[Chris Birkbeck]

I should also have some time next week to have a look