Commit 2024-10-17 20:34 78d236b3

View on Github →

feat(GroupTheory/GroupAction/Blocks): lemmas to handle blocks on finite sets (#14029) This PR proves specific properties of blocks when the action is on a finite set

Estimated changes

Modified Mathlib/GroupTheory/GroupAction/Blocks.lean

added theorem MulAction.IsBlock.eq_univ_card_lt

added theorem MulAction.IsBlock.ncard_block_eq_relindex

added theorem MulAction.IsBlock.ncard_block_mul_ncard_orbit_eq

added theorem MulAction.IsBlock.ncard_dvd_card

added theorem MulAction.IsBlock.of_subset

added theorem MulAction.IsBlock.subsingleton_of_card_lt

deleted theorem MulAction.isBlock_top

added theorem MulAction.isBlock_univ

deleted theorem MulAction.isFixedBlock_top

added theorem MulAction.isFixedBlock_univ

Modified Mathlib/GroupTheory/Index.lean

added theorem MulAction.index_stabilizer

added theorem MulAction.index_stabilizer_of_transitive