chore(FieldTheory.Ratfunc): forward-port #19133 (#4580) · leanprover-community/mathlib4@b4fa258 · GitHub

Commit

chore(FieldTheory.Ratfunc): forward-port #19133 (#4580)

Browse files

This PR re-ports `FieldTheory/RatFunc`, now that the mathlib3 version uses `section`s, after PR[#19133](leanprover-community/mathlib#19133).

This closes [#4513](#4513) and closes #4373.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Loading branch information

adomani and eric-wieser committed Jun 3, 2023

1 parent f055042 commit b4fa258