English
Let K be a nontrivially normed field and L a field with K-algebra structure, algebraic over K. Then L carries a norm defined by spectralNorm, turning L into a normed field.
Русский
Пусть K — ненулевое нормированное поле и L — поле с K-алгеброй, алгебраическое над K. Тогда на L задана норма через spectralNorm, и L становится нормированным полем.
LaTeX
$$$\|x\| := \mathrm{spectralNorm}(K,L,x)\quad \text{defines a norm on } L$$$
Lean4
/-- `L` with the spectral norm is a `NormedField`. -/
def normedField [CompleteSpace K] : NormedField L :=
{ (inferInstance : Field L) with
norm x := (spectralNorm K L x : ℝ)
dist x y := (spectralNorm K L (x - y) : ℝ)
dist_self x := by simp [sub_self, spectralNorm_zero]
dist_comm x y := by rw [← neg_sub, spectralNorm_neg (Algebra.IsAlgebraic.isAlgebraic _)]
dist_triangle x y z := sub_add_sub_cancel x y z ▸ isNonarchimedean_spectralNorm.add_le spectralNorm_nonneg
eq_of_dist_eq_zero
hxy := by
rw [← sub_eq_zero]
exact (map_eq_zero_iff_eq_zero (spectralMulAlgNorm K L)).mp hxy
dist_eq x y := rfl
norm_mul x y := by simp [← spectralMulAlgNorm_def, map_mul]
edist_dist x y := by rw [ENNReal.ofReal_eq_coe_nnreal] }
