Theorem NormedAddGroupHom.le_of_opNorm_le

Modification history

2023-03-17 14:06
Mathlib/Analysis/Normed/Group/Hom.lean
chore: tidy various files (#2950)
Added NormedAddGroupHom.le_of_opNorm_leView on Github →