Commit 2023-06-03 14:52 b4fa258e

View on Github →

chore(FieldTheory.Ratfunc): forward-port #19133 (#4580) This PR re-ports FieldTheory/RatFunc, now that the mathlib3 version uses sections, after PR[#19133](https://github.com/leanprover-community/mathlib/pull/19133). This closes [#4513](https://github.com/leanprover-community/mathlib4/issues/4513) and closes #4373.

Estimated changes

Modified Mathlib/FieldTheory/RatFunc.lean

modified def RatFunc.instAddCommGroup

modified def RatFunc.instCommMonoid

modified theorem RatFunc.ofFractionRing_add

modified theorem RatFunc.ofFractionRing_mul

modified theorem RatFunc.ofFractionRing_neg

modified theorem RatFunc.ofFractionRing_one

modified theorem RatFunc.ofFractionRing_sub

modified theorem RatFunc.ofFractionRing_zero

modified def RatFunc.toFractionRingRingEquiv

modified structure RatFunc