Skip to content

Comments

chore: bump mathlib#137

Merged
grunweg merged 7 commits intomasterfrom
bump
Jan 13, 2026
Merged

chore: bump mathlib#137
grunweg merged 7 commits intomasterfrom
bump

Conversation

@grunweg
Copy link
Collaborator

@grunweg grunweg commented Jan 12, 2026

Minor golfs, and remove now-upstreamed lemmas. Deal with two significant breaking changes:

  • updating smoothness lemmas from 1 ≤ n to n ≠ 0 hypothesis
  • updating from making ker take a LinearMap directly

@grunweg grunweg merged commit a2bd122 into master Jan 13, 2026
1 check passed
@grunweg grunweg deleted the bump branch January 13, 2026 16:36
grunweg pushed a commit that referenced this pull request Jan 13, 2026
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.

1 participant