Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ratfunc.to_fraction_ring_smul

Modification history

2022-06-30 19:45
src/field_theory/ratfunc.lean
refactor(algebra/group/defs): rename has_scalar to has_smul (#14559) …
Modified ratfunc.to_fraction_ring_smulView on Github →
2022-02-08 12:43
src/field_theory/ratfunc.lean
feat(*): localized `R[X]` notation for `polynomial R` (#11895) …
Modified ratfunc.to_fraction_ring_smulView on Github →
2021-12-16 10:58
src/field_theory/ratfunc.lean
chore(field_theory/ratfunc): has_scalar in terms of localization (#10828) …
Added ratfunc.to_fraction_ring_smulView on Github →