(add_/left_cancel_)semigroup

Stream: general

[Mario Carneiro]

If you search for both add_left_cancel_semigroup or left_cancel_add_semigroup you get a fair number of hits, like this one:

@[protected, instance]
def add_opposite.left_cancel_add_semigroup (α : Type u) [add_right_cancel_semigroup α] :
add_left_cancel_semigroup αᵃᵒᵖ

Mathlib seems to be of split mind on what the right order should be. This came up while checking the lean 4 name translations.