Theorem StrongDual.norm_extendRCLike_bound

Modification history

2026-02-25 03:11
Mathlib/Analysis/Normed/Module/RCLike/Extend.lean
refactor: improve API connecting `ℝ`- and `𝕜`-linear functionals (#34543) …
Added StrongDual.norm_extendRCLike_boundView on Github →