Theorem IsPowMul.map_one_le_one

Modification history

2025-05-27 21:58
Mathlib/Data/Real/Basic.lean
feat(Analysis/Normed/Unbundled/SpectralNorm): add spectral norm (#23301) …
Added IsPowMul.map_one_le_oneView on Github →