Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-15 17:00 5658241a

View on Github →

feat(ring_theory/localization,group_theory/monoid_localization): other scalar action instances (#10804) As requested by @pechersky. With this instance it's possible to state:

import field_theory.ratfunc
import data.complex.basic
import ring_theory.laurent_series
noncomputable example : ratfunc ℂ ≃ₐ[ℂ] fraction_ring (polynomial ℂ) := sorry

Estimated changes