Def IsUltrametricDist.algNormOfAlgEquiv

Modification history

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