Theorem Mul.to_covariant_class_left

Modification history

2022-11-13 23:39
Mathlib/Algebra/Order/Monoid.lean
CovariantClass naming fixes + #align (#590) …
Deleted Mul.to_covariant_class_leftView on Github →
2022-11-12 21:38
Mathlib/Algebra/Order/Monoid.lean
Revert "name covariant_class -> covariantClass + attribute" …
Added Mul.to_covariant_class_leftView on Github →
2022-11-12 20:45
Mathlib/Algebra/Order/Monoid.lean
name covariant_class -> covariantClass + attribute
Deleted Mul.to_covariant_class_leftView on Github →
2022-10-23 22:19
Mathlib/Algebra/Order/Monoid.lean
feat: partial port of Algebra/Order/ (#470) …
Added Mul.to_covariant_class_leftView on Github →