group_theory/subgroup/basic reduction #17862

Stream: PR reviews

[Ruben Van de Velde]

Does anyone want to review this before the rising tide engulfs it (maybe 10 PRs or so away)?

[Eric Wieser]

13 unported files and 2 in progress PRs away, according to https://leanprover-community.github.io/mathlib-port-status/

[Ruben Van de Velde]

Oh, cool page

[Riccardo Brasca]

I will have a look later today

[Riccardo Brasca]

Can you explain a little bit why this splitting is useful? I am not against it, it's just to be sure to understand the purpose of the PR.

[Ruben Van de Velde]

Just that the file is huge - top 5 of biggest files in mathlib, IIRC - and this seemed like a reasonable way to start doing something about it. "this is not worth it" would be a fine review too, as far as I'm concerned :)

[Riccardo Brasca]

Ah, I didn't notice is so big!

[Riccardo Brasca]

Wow, it's more than 3000 lines. Let's split it then.

[Riccardo Brasca]

Delegated. There is a line that I think has been forgotten.

[Ruben Van de Velde]

@Riccardo Brasca thanks - could you clarify your comment? I moved the description to src/group_theory/subgroup/simple.lean, though no longer as a bullet point

[Riccardo Brasca]

Exactly, I mean you could add a "main definition" section to that file.

[Ruben Van de Velde]

Done, thanks. I merged master for good measure, will put it on the queue when CI comes back