Skip to content

feat: extend the topological vector space section - #29

Merged
Vierkantor merged 3 commits into
leanprover-community:mainfrom
mcdoll:tvs
Oct 13, 2026
Merged

Vierkantor merged 3 commits into
leanprover-community:mainfrom
mcdoll:tvs

Conversation

@mcdoll

@mcdoll mcdoll commented Sep 24, 2026 •

Copy link
Copy Markdown
Member

Expand a the section on TVS, with better explanation of the differences between the three spellings, different topologies on continuous linear maps

@mcdoll
mcdoll marked this pull request as ready for review September 30, 2026 02:52
@mcdoll mcdoll changed the title extend the topological vector space section feat: extend the topological vector space section Sep 30, 2026
Comment thread Phrasebook/TVS.lean Outdated

@Vierkantor Vierkantor left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm trusting you on the mathematical contents, the phrasing looks good. About the "wip" in the PR description, are you planning to add more to this PR still?

@mcdoll

mcdoll commented Oct 11, 2026

Copy link
Copy Markdown
Member Author

Sorry, forgot about changing that.

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

@Vierkantor Vierkantor left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! I checked this builds after the bump to v4.35.0. Let's merge this 🎉

@Vierkantor
Vierkantor merged commit 953d92e into leanprover-community:main Oct 13, 2026
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants