Commit 2025-02-14 15:54 adf649c0
View on Github →feat: FunLike instance for HilbertBasis (#21440)
Hilbert bases are equal iff their elements are equal.
This is obtained from a more general ext lemma for continuous additive maps from lp.
Many helper lemmas for lp.single are added / generalized / golfed along the way.