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

Estimated changes

deleted theorem MulAction.IsBlock.def
deleted theorem MulAction.IsBlock.def_mem
deleted theorem MulAction.IsBlock.def_one
modified theorem MulAction.IsBlock.iInter
deleted theorem MulAction.IsBlock.iff_top
modified theorem MulAction.IsBlock.inter
deleted theorem MulAction.IsBlock.mk_mem
modified theorem MulAction.IsBlock.preimage
modified theorem MulAction.IsBlock.subgroup
modified theorem MulAction.IsBlock.translate
added theorem MulAction.IsBlock.univ
modified def MulAction.IsBlock
deleted theorem MulAction.isBlock_empty
deleted theorem MulAction.isBlock_orbit
added theorem MulAction.isBlock_top
deleted theorem MulAction.isBlock_univ