Commit 2024-05-28 17:51 803d28ff
View on Github →Feat (GroupTheory/GroupAction/Blocks) : blocks for a mul action (#12049) This PR defines the notion of a block for a mul action and establishes various basic lemmas, as well as alternative versions of the definition. Blocks are used to define primitive actions, which appear as an hypothesis of the Iwasawa criterion for simplicity.