Spectral norm of transcendental elements

For an element of a field extension that is transcendental over a normed field K, the minimal polynomial is zero, so its spectral norm over K is zero.

Main results

• TauCeti.spectralNorm_eq_zero_of_not_isAlgebraic: the spectral norm over K of an element that is transcendental over K is zero.

theorem TauCeti.spectralNorm_eq_zero_of_not_isAlgebraic {K : Type u_1} [NormedField K] {L : Type u_2} [Field L] [Algebra K L] {y : L} (hy : ¬IsAlgebraic K y) : spectralNorm K L y = 0

The spectral norm of an element that is transcendental over K is zero, since its minimal polynomial is 0.