eq_of_tower — Mathlib

English

For any polynomial p, spectralValue(p) ≥ 0.

Русский

Для любого полинома p ∈ R[X], spectralValue(p) ≥ 0.

LaTeX

$$$$0 \le \operatorname{spectralValue}(p).$$$$

Lean4

/-- If `L/E/K` is a tower of fields, then the spectral norm of `x : E` equals its spectral norm
  when regarding `x` as an element of `L`. -/
theorem eq_of_tower {E : Type*} [Field E] [Algebra K E] [Algebra E L] [IsScalarTower K E L] (x : E) :
    spectralNorm K E x = spectralNorm K L (algebraMap E L x) :=
  by
  have hx : minpoly K (algebraMap E L x) = minpoly K x := minpoly.algebraMap_eq (algebraMap E L).injective x
  simp only [spectralNorm, hx]

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