Theorem LinearEquiv.extendOfIsometry_symm_apply

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