Theorem LinearEquiv.extend_eq

Modification history

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