Hahn banach 2026#1889

Merged

affeldt-aist merged 48 commits into

math-comp:masterfrom

mkerjean:hahn_banach_2026

Jun 9, 2026

Commits on Jun 8, 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
add nix bundle 9.1-master and upd nix toolbox
affeldt-aist
committed
upd nix
affeldt-aist
committed
fix
affeldt-aist
committed
upd ci
affeldt-aist
committed
upd nix toolbox
affeldt-aist
committed
fix ci
affeldt-aist
committed
upd changelog
affeldt-aist
committed

Commits on Jun 9, 2026