Theorem MvPowerSeries.ultrametric_strict

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