Commit 2024-10-22 16:09 c6021b7b
View on Github →refactor(GroupAction/Blocks): additivise, fix names, golf API (#17578)
Most of the API can be additivised smoothly. The lemma names didn't match the naming convention. Some proofs were harder than necessary because of the suboptimal definition of IsBlock as ∀ _, _ ∨ _ rather than ∀ _, _ → _.
From LeanCamCombi