Theorem IsUltrametricDist.isPowMul_algNormOfAlgEquiv

Modification history

2025-05-14 16:03
Mathlib/Analysis/Normed/Unbundled/InvariantExtension.lean
feat(Analysis/Normed/Unbundled/AlgNormOfAut): add algNormOfAut (#23184) …
Added IsUltrametricDist.isPowMul_algNormOfAlgEquivView on Github →