Theorems · Theorem · commutative algebra

spectralNorm_neg

∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] [IsUltrametricDist K]
  {y : L}, IsAlgebraic K y → spectralNorm K L (-y) = spectralNorm K L y

spectralNorm K L (-y) = spectralNorm K L y .

Defined in

Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Cited by

0 results in Mathlib

Foundations

Depth 223 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedFieldFieldAlgebraIsUltrametricDist