Skip to content

[Merged by Bors] - feat: Lie bracket with zero is zero#26734

Closed
grunweg wants to merge 8 commits intoleanprover-community:masterfrom
grunweg:liebracket-zero
Closed

[Merged by Bors] - feat: Lie bracket with zero is zero#26734
grunweg wants to merge 8 commits intoleanprover-community:masterfrom
grunweg:liebracket-zero

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Jul 4, 2025


Open in Gitpod

@github-actions github-actions bot added the t-analysis Analysis (normed *, calculus) label Jul 4, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 4, 2025

PR summary c14c4461ad

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ lieBracketWithin_zero_left
+ lieBracketWithin_zero_right
+ lieBracket_zero_left
+ lieBracket_zero_right
+ mlieBracketWithin_zero_left
+ mlieBracketWithin_zero_right
+ mlieBracket_zero_left
+ mlieBracket_zero_right
+ mpullbackWithin_zero
+ mpullback_zero

You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.


No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@grunweg grunweg added the t-differential-geometry Manifolds etc label Jul 4, 2025
@grunweg grunweg mentioned this pull request Jul 4, 2025
35 tasks
@grunweg grunweg changed the title feat: lieBracket with zero is zero feat: Lie bracket with zero is zero Jul 4, 2025
@sgouezel sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 5, 2025
grunweg and others added 5 commits July 6, 2025 01:02
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Jul 5, 2025

Thanks for the helpful review; I have hopefully addressed everything again.

@grunweg grunweg removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 6, 2025
@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Jul 7, 2025

bors r+
Thanks!

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jul 7, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jul 7, 2025
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 7, 2025

Pull request successfully merged into master.

Build succeeded:

  • CI Success

@mathlib-bors mathlib-bors bot changed the title feat: Lie bracket with zero is zero [Merged by Bors] - feat: Lie bracket with zero is zero Jul 7, 2025
@mathlib-bors mathlib-bors bot closed this Jul 7, 2025
@grunweg grunweg deleted the liebracket-zero branch July 7, 2025 10:37
BeibeiX0 pushed a commit to BeibeiX0/mathlib4 that referenced this pull request Jul 16, 2025
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
hrmacbeth pushed a commit to szqzs/mathlib4 that referenced this pull request Jul 28, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus) t-differential-geometry Manifolds etc

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants