Theorem Module.Dual.exists_extension_of_le_seminorm_real

Modification history

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