mathlib3
5658241a - feat(ring_theory/localization,group_theory/monoid_localization): other scalar action instances (#10804)

Commit
4 years ago
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: ```lean import field_theory.ratfunc import data.complex.basic import ring_theory.laurent_series noncomputable example : ratfunc ℂ ≃ₐ[ℂ] fraction_ring (polynomial ℂ) := sorry ```
Author
Parents
Loading