Theorem IsUltrametricDist.invariantExtension_apply

Modification history

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