Theorem LinearEquiv.norm_extend_le

Modification history

2025-12-02 23:02
Mathlib/Analysis/Normed/Operator/Extend.lean
feat(Analysis/Normed): extension to linear isometry equivalence (#31076) …
Added LinearEquiv.norm_extend_leView on Github →