English
For any algebraic y, spectralNorm(-y) = spectralNorm(y).
Русский
Для любого алгебраического элемента y верно spectralNorm(-y) = spectralNorm(y).
LaTeX
$$$\operatorname{spectralNorm}_{K,L}(-y) = \operatorname{spectralNorm}_{K,L}(y) \quad(\text{для всех } y\text{ алгебраических})$$$
Lean4
/-- `spectralNorm K L (-y) = spectralNorm K L y` . -/
theorem spectralNorm_neg {y : L} (hy : IsAlgebraic K y) : spectralNorm K L (-y) = spectralNorm K L y :=
by
set E := K⟮y⟯
haveI h_finiteDimensional_E : FiniteDimensional K E := IntermediateField.adjoin.finiteDimensional hy.isIntegral
set g := IntermediateField.AdjoinSimple.gen K y
have hy : -y = (algebraMap K⟮y⟯ L) (-g) := rfl
rw [← spectralNorm.eq_of_normalClosure g (IntermediateField.AdjoinSimple.algebraMap_gen K y), hy, ←
spectralNorm.eq_of_normalClosure (-g) hy, RingHom.map_neg, ← spectralAlgNorm_of_finiteDimensional_normal_def]
exact map_neg_eq_map _ _
