Skip to content

Sums in normed real vector spaces#1940

Open
lowasser wants to merge 8 commits into
UniMath:masterfrom
lowasser:sums-real-vec
Open

Sums in normed real vector spaces#1940
lowasser wants to merge 8 commits into
UniMath:masterfrom
lowasser:sums-real-vec

Conversation

@lowasser
Copy link
Copy Markdown
Collaborator

Comes with a lot of other pieces all over linear-algebra, but they're mostly very formulaic (copying properties from the next layer of abstraction down).

@lowasser
Copy link
Copy Markdown
Collaborator Author

This can probably be broken up further if it'd help.

@lowasser lowasser marked this pull request as draft April 24, 2026 00:18
EgbertRijke pushed a commit that referenced this pull request Apr 27, 2026
@lowasser lowasser marked this pull request as ready for review May 1, 2026 00:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant