Theorem LinearMap.norm_extendTođť•ś'_apply_sq

Modification history

2025-09-18 17:28
Mathlib/Analysis/NormedSpace/Extend.lean
chore(Analysis/NormedSpace/Extend): split file (#29445) …
Modified LinearMap.norm_extendTo𝕜'_apply_sqView on Github →
2023-05-19 05:51
Mathlib/Analysis/NormedSpace/Extend.lean
feat: port Analysis.NormedSpace.Extend (#4069)
Added LinearMap.norm_extendTo𝕜'_apply_sqView on Github →