Theorem MvPowerSeries.Finset.Nonempty.map_sum_le_sup'_map

Modification history

2026-06-17 10:37
Mathlib/RingTheory/MvPowerSeries/GaussNorm.lean
feat: lemmas towards showing gaussNorm on MvPowerSeries is an absolute value (#38049) …
Added MvPowerSeries.Finset.Nonempty.map_sum_le_sup'_mapView on Github →