Theorem LinearEquiv.extendOfIsometry_symm_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.extendOfIsometry_symm_eqView on Github →