Theorem IsUltrametricDist.isNonarchimedean_invariantExtension

Modification history

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