Theorem spectralNorm_eq_of_equiv

Modification history

2025-10-16 07:33
Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean
feat: notation for galois group (#30266) …
Modified spectralNorm_eq_of_equivView on Github →
2025-05-27 21:58
Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean
feat(Analysis/Normed/Unbundled/SpectralNorm): add spectral norm (#23301) …
Added spectralNorm_eq_of_equivView on Github →