Theorem MvPowerSeries.antidiagonal_dominant

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