Commit 2023-12-09 09:17 aa99c9f6

View on Github →

refactor: Remove leftCoset/rightCoset (#8877) Those two definitions are completely obsolete now that we have the pointwise API. This PR removes them but not the corresponding API. A much more tedious subsequent PR will be needed to merge the two API. Note that I need to tweak simp lemmas to keep confluence since I'm merging two pairs of head keys together.

Estimated changes

modified theorem eq_cosets_of_normal
deleted def leftCoset
modified theorem leftCoset_assoc
modified theorem leftCoset_eq_iff
modified theorem leftCoset_mem_leftCoset
modified theorem leftCoset_rightCoset
modified theorem mem_leftCoset
modified theorem mem_leftCoset_iff
modified theorem mem_leftCoset_leftCoset
modified theorem mem_own_leftCoset
modified theorem mem_own_rightCoset
modified theorem mem_rightCoset
modified theorem mem_rightCoset_iff
modified theorem mem_rightCoset_rightCoset
modified theorem normal_iff_eq_cosets
modified theorem normal_of_eq_cosets
modified theorem one_leftCoset
deleted def rightCoset
modified theorem rightCoset_assoc
modified theorem rightCoset_eq_iff
modified theorem rightCoset_mem_rightCoset
modified theorem rightCoset_one
added theorem op_smul_coe_set
added theorem smul_coe_set
modified theorem IsClosed.leftCoset
modified theorem IsClosed.rightCoset
modified theorem IsOpen.leftCoset
modified theorem IsOpen.rightCoset