Joe Hendrix 8293fd4e09 feat: cleanups to ACI and Identity classes (#3195) ... This makes changes to the definitions of Associativity, Commutativity, Idempotence and Identity classes to be more aligned with Mathlib's versions. The changes are: * Move classes are moved from `Lean` to root namespace. * Drop `Is` prefix from names. * Rename `IsNeutral` to `LawfulIdentity` and add Left and Right subclasses. * Change neutral/identity element to outParam. * Introduce `HasIdentity` for operations not intended for proofs to implement The identity changes are to make this compatible with [Mathlib](718042db9d/Mathlib/Init/Algebra/Classes.lean) and to enable nicer fold operations in Std that can use type classes to infer the identity/initial element on binary operations. --------- Co-authored-by: Kyle Miller <kmill31415@gmail.com>		2024-01-24 21:46:58 +00:00
..
Main.lean	feat: cleanups to ACI and Identity classes (#3195)	2024-01-24 21:46:58 +00:00