Theorem IsUltrametricDist.isPowMul_invariantExtension

Modification history

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