Def LinearEquiv.extend

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 View on Github →