Commit 2022-01-16 13:30 1aee8a8d

View on Github →

chore(*): Put simp attribute before to_additive (#11488) A few lemmas were tagged in the wrong order. As tags are applied from left to right, @[to_additive, simp] only marks the multiplicative lemma as simp. The correct order is thus @[simp, to_additive].

Estimated changes

Modified src/algebra/group/opposite.lean

modified theorem mul_opposite.commute_op

modified theorem mul_opposite.commute_unop

Modified src/algebra/order/lattice_group.lean

Modified src/group_theory/submonoid/inverses.lean

modified theorem submonoid.from_left_inv_eq_inv

modified theorem submonoid.from_left_inv_left_inv_equiv_symm

modified theorem submonoid.from_left_inv_one

modified theorem submonoid.left_inv_equiv_symm_eq_inv

modified theorem submonoid.left_inv_equiv_symm_from_left_inv

modified theorem submonoid.left_inv_equiv_symm_mul

modified theorem submonoid.mul_left_inv_equiv_symm