Commit 2025-10-14 10:22 60a1d0a5

View on Github →

feat(Analysis/Normed/Unbundled/SpectralNorm): add API (#26668)

Estimated changes

Modified Mathlib/Algebra/Polynomial/FieldDivision.lean

added theorem Polynomial.monic_mapAlg_iff

Modified Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean

modified theorem spectralAlgNorm_mul

modified def spectralMulAlgNorm

modified theorem spectralMulAlgNorm_def

modified def spectralNorm.metricSpace

modified def spectralNorm.normedAddCommGroup

modified def spectralNorm.normedField

modified def spectralNorm.normedSpace

modified def spectralNorm.seminormedAddCommGroup

added theorem spectralNorm.spectralMulAlgNorm_eq_of_mem_roots

added theorem spectralNorm.spectralNorm_eq_norm_coeff_zero_rpow

added theorem spectralNorm.spectralNorm_pow_natDegree_eq_prod_roots

modified def spectralNorm.uniformSpace

added theorem spectralValue_le_one_iff