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.

Estimated changes