Commit 2022-11-13 23:39 63c7bb14

View on Github →

CovariantClass naming fixes + #align (#590) Correct PR compared against master, incorporating suggestions to previous PR

Estimated changes

Modified Mathlib/Algebra/Order/Group.lean

Modified Mathlib/Algebra/Order/Monoid.lean

added theorem Mul.to_covariantClass_left

added theorem Mul.to_covariantClass_right

deleted theorem Mul.to_covariant_class_left

deleted theorem Mul.to_covariant_class_right