Zulip Chat Archive

Stream: general

Topic: (add_/left_cancel_)semigroup


Mario Carneiro (Nov 20 2022 at 12:45):

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.


Last updated: Dec 20 2023 at 11:08 UTC