mathlib3
b599f4e4 - chore(algebra/order/group/defs): remove some instances that cause timeouts with etaExperiment (#18985)

Commit
2 years ago
chore(algebra/order/group/defs): remove some instances that cause timeouts with etaExperiment (#18985) Seeing what CI thinks about removing these instances. This is a backport of https://github.com/leanprover-community/mathlib4/pull/3905 Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Author
Parents
Loading