Theorem Module.Dual.norm_extendRCLike_le_seminorm

Modification history

2026-06-11 01:51
Mathlib/Analysis/Normed/Module/RCLike/Extend.lean
feat: Analytic Hahn Banach theorem for locally convex spaces (#38739) …
Added Module.Dual.norm_extendRCLike_le_seminormView on Github →