Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-09 20:16 a02ab48a

View on Github →

refactor(group_theory/subgroup): swap mul_mem_cancel_left/right (#3011) This way the name follows the position of the term we cancel.

Estimated changes

Modified src/deprecated/subgroup.lean

modified theorem is_subgroup.mul_mem_cancel_left

modified theorem is_subgroup.mul_mem_cancel_right

Modified src/group_theory/coset.lean

Modified src/group_theory/order_of_element.lean

Modified src/group_theory/quotient_group.lean

Modified src/group_theory/subgroup.lean

added theorem subgroup.inv_mem_iff

modified theorem subgroup.mul_mem_cancel_left

modified theorem subgroup.mul_mem_cancel_right

Modified src/group_theory/sylow.lean