Theorem MulAction.IsBlock.ncard_block_mul_ncard_orbit_eq

Modification history

2024-10-17 20:34
Mathlib/GroupTheory/GroupAction/Blocks.lean
feat(GroupTheory/GroupAction/Blocks): lemmas to handle blocks on finite sets (#14029) …
Added MulAction.IsBlock.ncard_block_mul_ncard_orbit_eqView on Github →