Theorem MvPowerSeries.coeff_embDomain_rename

Modification history

2026-03-11 00:43
Mathlib/RingTheory/MvPowerSeries/Rename.lean
feat(RingTheory/MvPowerSeries): introduce `rename` (#33188) …
Added MvPowerSeries.coeff_embDomain_renameView on Github →