Def MvPowerSeries.renameFun

Modification history

2026-04-19 00:33

Mathlib/RingTheory/MvPowerSeries/Rename.lean

chore: adaptations for overlapping instances linter (#38151) …

Modified MvPowerSeries.renameFun View on Github →

2026-03-11 00:43

Mathlib/RingTheory/MvPowerSeries/Rename.lean

feat(RingTheory/MvPowerSeries): introduce `rename` (#33188) …

Added MvPowerSeries.renameFun View on Github →