Hahn banach 2026#1889

Draft

mkerjean wants to merge 18 commits intomath-comp:masterfrom

mkerjean:hahn_banach_2026

Commits on Mar 25, 2026

linfun and lcfun are lmodtypes

mkerjean
and
CohenCyril
committed
uncomment and make compile

affeldt-aist
authored and
mkerjean
committed
Apply suggestion from @affeldt-aist

affeldt-aist
authored and
mkerjean
committed
Apply suggestion from @affeldt-aist

affeldt-aist
authored and
mkerjean
committed
fix

affeldt-aist
authored and
mkerjean
committed
generalization

authored and
mkerjean
committed
fix

affeldt-aist
authored and
mkerjean
committed
mv convex

affeldt-aist
authored and
mkerjean
committed
mv convex

affeldt-aist
authored and
mkerjean
committed
hahn_banach thm file
mkerjean
committed
convex functions wip i01
mkerjean
committed
lemmas i01 and fix
mkerjean
committed
sup and inf from realtype
mkerjean
committed
F : subLmodType
mkerjean
committed
clean proof
mkerjean
committed
fix subLmodType
mkerjean
committed
subnormed
mkerjean
committed
to be rebased on linear_continuous
mkerjean
committed