2025-03-04 17:12
Mathlib/Analysis/Normed/Ring/FiniteExtension.lean
feat(Analysis.Normed.Ring.FiniteExtension): prove existence of nonarchimedean power multiplicative norm on finite extension (#22081) …
Added exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional