Hahn banach 2026#1889

Open

mkerjean wants to merge 36 commits into

math-comp:masterfrom

mkerjean:hahn_banach_2026

Commits on May 18, 2026

Hahn-Banach theorem

mkerjean
authored and
affeldt-aist
committed
minor linting
affeldt-aist
committed
definition of sub normed module
affeldt-aist
committed
todo

mkerjean
authored and
affeldt-aist
committed
subNormedModType factory

mkerjean
authored and
affeldt-aist
committed
subNormedModType

mkerjean
authored and
affeldt-aist
committed
fail subconvextvs

mkerjean
authored and
affeldt-aist
committed
clean

mkerjean
authored and
affeldt-aist
committed
filter by hand (still broken)
affeldt-aist
committed
instances instead of factories

mkerjean
authored and
affeldt-aist
committed
subConvexTvsType at last
affeldt-aist
committed
proofs

mkerjean
authored and
affeldt-aist
committed
proofs

mkerjean
authored and
affeldt-aist
committed
proofs

mkerjean
authored and
affeldt-aist
committed
proofs

mkerjean
authored and
affeldt-aist
committed
proofs

mkerjean
authored and
affeldt-aist
committed
simplification of add_sub
affeldt-aist
committed
base convexe wip

mkerjean
authored and
affeldt-aist
committed
base convexe wip

mkerjean
authored and
affeldt-aist
committed
base convexe wip

mkerjean
authored and
affeldt-aist
committed
missing join ?

mkerjean
authored and
affeldt-aist
committed
sub locally convex

mkerjean
authored and
affeldt-aist
committed
lint
affeldt-aist
committed
fix
affeldt-aist
committed
upd changelog (wip)
affeldt-aist
committed
fix changelog
affeldt-aist
committed
all_ssreflect -> all_{boot,order}
affeldt-aist
committed
trying to green CI
affeldt-aist
committed
dummy structure to cheat the CI
affeldt-aist
committed
add doc
affeldt-aist
committed
fix changelog
affeldt-aist
committed
fix changelog
affeldt-aist
committed
fix changelog
affeldt-aist
committed
fix changelog
affeldt-aist
committed
deleting comments

mkerjean
authored and
affeldt-aist
committed
finalize changelog and doc
affeldt-aist
committed