Mario Carneiro (Nov 20 2022 at 12:45):
If you search for both
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: Aug 03 2023 at 10:10 UTC