Theorem MulAction.isBlock_iff_smul_eq_smul_of_nonempty

Modification history

2024-10-22 16:09
Mathlib/GroupTheory/GroupAction/Blocks.lean
refactor(GroupAction/Blocks): additivise, fix names, golf API (#17578) …
Added MulAction.isBlock_iff_smul_eq_smul_of_nonemptyView on Github →