Hahn banach 2026#1889

Draft

mkerjean wants to merge 33 commits intomath-comp:masterfrom

mkerjean:hahn_banach_2026

Commits on Mar 31, 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
notations
mkerjean
committed
doc and changelog
mkerjean
committed

Commits on Apr 3, 2026

clean
mkerjean
committed
wip
affeldt-aist
committed
check
affeldt-aist
committed
fix
affeldt-aist
committed
fix
affeldt-aist
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
wip subnormed
mkerjean
committed
wip linear continuous
mkerjean
committed
wip linear_continuous
mkerjean
committed
clean
mkerjean
committed
substructures tentative
mkerjean
committed
fix
mkerjean
committed
clean
mkerjean
committed
clean and tentative doc
mkerjean
committed