Commit 2023-06-01 08:55 67237461
View on Github →chore(field_theory/ratfunc): use section
instead of omit/include
(#19133)
This hopefully closes [#4513](https://github.com/leanprover-community/mathlib4/issues/4513) (or at least mitigates it) and will settle [!4#4373](https://github.com/leanprover-community/mathlib4/pull/4373) in mathlib3.