Commit 2025-05-14 16:03 c61b9b01

feat(Analysis/Normed/Unbundled/AlgNormOfAut): add algNormOfAut (#23184) Let K be a nonarchimedean normed field and L/K be a finite extension. We show that the function L → ℝ sending x : L to the maximum of ‖ σ x ‖ over all σ : L ≃ₐ[K] L is an algebra norm on L. We also prove that this algebra norm is power multiplicative, nonarchimedean, and extends the norm on K.