mathlib3
67237461 - chore(field_theory/ratfunc): use `section` instead of `omit/include` (#19133)

Commit
2 years ago
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. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Author
Parents
Loading