Note about deprecated files

This file is deprecated, and is no longer imported by anything in mathlib other than other deprecated files, and test files. You should not need to import it.

Unbundled algebra classes

These classes were part of an incomplete refactor described here on the github Wiki. However a subset of them are widely used in mathlib3, and it has been tricky to clean this up as this file was in core Lean 3.

@[deprecated "No deprecation message was provided." (since := "2024-09-11")]

class IsLeftCancel (α : Sort u) (op : α → α → α) : Prop

• left_cancel (a b c : α) : op a b = op a c → b = c

@[deprecated "No deprecation message was provided." (since := "2024-09-11")]

class IsRightCancel (α : Sort u) (op : α → α → α) : Prop

• right_cancel (a b c : α) : op a b = op c b → a = c