chore(combinatorics/young_tableau): move young_diagram.lean into young_tableau directory

Open jakelev opened this issue 3 years ago • 2 comments

Rename combinatorics/young_tableaux directory to combinatorics/young_tableau. Move combinatorics/young_diagram.lean to combinatorics/young_tableau/young_diagram.lean.

This is to group all topics related to Young tableaux together. Future additions will be in this directory.

Oct 13 '22 16:10 jakelev

What about combinatorics.young.semistandard_tableau/combinatorics.young.diagram?

Oct 13 '22 17:10 YaelDillies

What about combinatorics.young.semistandard_tableau/combinatorics.young.diagram?

That would be fine with me as long as it's in keeping with mathlib conventions (which I am not knowledgeable about). I would still prefer to have the objects themselves to be structure young_diagram and structure ssyt.

Oct 13 '22 19:10 jakelev

Thanks!

bors r+

Oct 14 '22 14:10 kmill

Pull request successfully merged into master.

Build succeeded:

Oct 14 '22 16:10 bors[bot]