Skip to content

feat(QM) : Add polyBddSchwartzSubmodule coercions#1071

Merged
jstoobysmith merged 6 commits intoleanprover-community:masterfrom
gloges:schwartz
May 3, 2026
Merged

feat(QM) : Add polyBddSchwartzSubmodule coercions#1071
jstoobysmith merged 6 commits intoleanprover-community:masterfrom
gloges:schwartz

Conversation

@gloges
Copy link
Copy Markdown
Contributor

@gloges gloges commented May 2, 2026

  • Adds Schwartz maps and function coercions.
  • Adds (PolyBdd)SchwartzSubmodule namespaces and simplifies some lemma names.
  • Relocates tendsto_zero_iff_tendsto_zero_lintegral_enorm_sq.

@gloges
Copy link
Copy Markdown
Contributor Author

gloges commented May 2, 2026

t-quantum-mechanics

Copy link
Copy Markdown
Member

@jstoobysmith jstoobysmith left a comment

Choose a reason for hiding this comment

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

Makes sense. Approved, and will merge shortly.

@jstoobysmith jstoobysmith added the ready-to-merge This PR is approved and will be merged shortly label May 2, 2026
@jstoobysmith jstoobysmith merged commit 1e4214d into leanprover-community:master May 3, 2026
4 checks passed
@gloges gloges deleted the schwartz branch May 3, 2026 12:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR is approved and will be merged shortly t-quantum-mechanics Quantum mechanics

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants