Theorem MvPowerSeries.gaussNorm_mul_le

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_mul_leView on Github →