Def LinearEquiv.extendOfIsometry

Modification history

2025-12-02 23:02

Mathlib/Analysis/Normed/Operator/Extend.lean

feat(Analysis/Normed): extension to linear isometry equivalence (#31076) …

Added LinearEquiv.extendOfIsometry View on Github →