Commit 2024-09-15 08:25 a219fbf7
View on Github →refactor: Logic.OpClass
(#16748)
Put IsSymmOp
, LeftCommutative
and RightCommutative
under a new file Logic.OpClass
. This has the effect of completely deprecating Init.Algebra.Classes
.
All remaining undeprecated Init
code now consists of attributes and relational definitions in Init.Logic
. One instance that is not needed anywhere in mathlib and that would cause a dependency of Logic.OpClass
on Order.Defs
has been removed.