Theorem ContinuousLinearMap.norm_extendTođť•ś'_bound

Modification history

2026-02-25 03:11
Mathlib/Analysis/Normed/Module/RCLike/Extend.lean
refactor: improve API connecting `ℝ`- and `𝕜`-linear functionals (#34543) …
Deleted ContinuousLinearMap.norm_extendTo𝕜'_boundView on Github →
2025-09-18 17:28
Mathlib/Analysis/Normed/Module/RCLike/Extend.lean
chore(Analysis/NormedSpace/Extend): split file (#29445) …
Modified ContinuousLinearMap.norm_extendTo𝕜'_boundView on Github →
2025-08-22 20:24
Mathlib/Analysis/NormedSpace/Extend.lean
refactor: Use `StrongDual` (#28726) …
Modified ContinuousLinearMap.norm_extendTo𝕜'_boundView on Github →
2023-05-19 05:51
Mathlib/Analysis/NormedSpace/Extend.lean
feat: port Analysis.NormedSpace.Extend (#4069)
Added ContinuousLinearMap.norm_extendTo𝕜'_boundView on Github →