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