Archive.100-theorems-list.XXTheoremName causes error !4#5114

Stream: mathlib4

[Pol'tta / Miyahara Kō]

I suggest renaming to Archive.Wiedijk100Theorems.TheoremName.

[Johan Commelin]

Sounds good to me.

[Johan Commelin]

Do you want to make a corresponding PR to ml3 so that mathport takes care of the rest of the renaming?

[Pol'tta / Miyahara Kō]

Probably, I have no premission to create PRs for Mathlib 3.

[Johan Commelin]

Aah, I can fix that

[Johan Commelin]

@Pol'tta / Miyahara Kō https://github.com/leanprover-community/mathlib/invitations

[Pol'tta / Miyahara Kō]

I've created the PR:
https://github.com/leanprover-community/mathlib/pull/19195