eq_zero_of_map_spectralNorm_eq_zero

English

If spectralNorm(K,L)(x) = 0 and x is algebraic over K, then x = 0.

Русский

Если spectralNorm(K,L)(x)=0 и x алгебраически над K, то x=0.

LaTeX

$$$$\operatorname{spectralNorm}(K,L)(x)=0 \Rightarrow x=0.$$$$

Lean4

/-- If `spectralNorm K L x = 0`, then `x = 0`. -/
theorem eq_zero_of_map_spectralNorm_eq_zero {x : L} (hx : spectralNorm K L x = 0) (hx_alg : IsAlgebraic K x) : x = 0 :=
  by
  by_contra h0
  exact (ne_of_gt (spectralNorm_zero_lt h0 hx_alg)) hx

Похожие утверждения