feat(GroupTheory/GroupAction/Blocks): order iso between blocks and subgroups

[AntoineChambert-Loir]

This PR proves the order isomorphism between blocks containing a point and subgroups containing its stabilizer.

---

This is a new branch to correct the bad merge of #12050

[github-actions[bot]]

PR summary e4c484914c

Import changes

No significant changes to the import graph

---

Declarations diff

+ IsBlock.of_orbit + IsBlock.orbit_stabilizer_eq + IsBlock.stabilizer_le + block_stabilizerOrderIso + stabilizer_orbit_eq

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[mathlib-bors[bot]]

:v: AntoineChambert-Loir can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[AntoineChambert-Loir]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style