lean4-htt/src/Init/Grind/Ring
Kim Morrison dfcb5bb3a8
chore: remove a bad grind algebra instance (#10324)
This PR disables an unused instance that causes expensive typeclass
searches.
2025-09-11 06:44:47 +00:00
..
Basic.lean chore: use SMul rather than HMul in grind algebra typeclasses (#10095) 2025-08-26 12:23:37 +00:00
Envelope.lean chore: replace Lean.Grind internal preorder classes with the classes from Std (#10129) 2025-08-26 13:18:22 +00:00
Field.lean chore: remove a bad grind algebra instance (#10324) 2025-09-11 06:44:47 +00:00
OfSemiring.lean chore: eliminate uses of intros x y z (#9983) 2025-08-19 06:09:13 +00:00
Poly.lean feat: (approximate) inverses of dyadic rationals (#10194) 2025-09-02 03:43:53 +00:00
ToInt.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00