Theorem MvPowerSeries.gaussNorm_le_mul

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.gaussNorm_le_mulView on Github →