spectralNorm_zero_lt — Mathlib

English

If y ≠ 0 and y is algebraic over K, then spectralNorm(K,L,y) > 0.

Русский

Если y ≠ 0 и y алгебраически over K, то spectralNorm(K,L,y) > 0.

LaTeX

$$$$0 < \operatorname{spectralNorm}(K,L)(y).$$$$

Lean4

/-- `spectralNorm K L y` is positive if `y ≠ 0`. -/
theorem spectralNorm_zero_lt {y : L} (hy : y ≠ 0) (hy_alg : IsAlgebraic K y) : 0 < spectralNorm K L y :=
  by
  apply lt_of_le_of_ne (spectralNorm_nonneg _)
  rw [spectralNorm, ne_eq, eq_comm, spectralValue_eq_zero_iff (minpoly.monic hy_alg.isIntegral)]
  intro h
  apply minpoly.coeff_zero_ne_zero hy_alg.isIntegral hy
  rw [h, coeff_X_pow, if_neg (ne_of_lt (minpoly.natDegree_pos hy_alg.isIntegral))]

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