Commit 2023-05-16 03:29 f5551f22

View on Github →

chore: disable instances causing trouble with etaExperiment (#3905)

Estimated changes

Modified Mathlib/Algebra/Order/Group/Defs.lean

added theorem OrderedCommGroup.to_contravariantClass_left_le

added theorem OrderedCommGroup.to_contravariantClass_right_le