Commit 2022-11-12 20:45 2b62592b

View on Github →

name covariant_class -> covariantClass + attribute

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