Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-16 16:16 905d887f

View on Github →

chore(field_theory/ratfunc): to_fraction_ring_ring_equiv (#10806) Rename the underlying ratfunc.aux_equiv for discoverability.

Estimated changes

Modified src/field_theory/ratfunc.lean

deleted def ratfunc.aux_equiv

deleted theorem ratfunc.aux_equiv_eq

added def ratfunc.to_fraction_ring_ring_equiv

added theorem ratfunc.to_fraction_ring_ring_equiv_symm_eq