Skip to content

jmc lie theorem diff#20443

Merged
jcommelin merged 54 commits intolwhitfield-Lie-theoremfrom
jmc-lie-theorem-diff
Jan 3, 2025
Merged

jmc lie theorem diff#20443
jcommelin merged 54 commits intolwhitfield-Lie-theoremfrom
jmc-lie-theorem-diff

Conversation

@jcommelin
Copy link
Copy Markdown
Member

@jcommelin jcommelin commented Jan 3, 2025


Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 3, 2025

PR summary 0d9b8bd2cf

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Algebra.Lie.LieTheorem (new file) 1473

Declarations diff

+ exists_forall_lie_eq_smul_of_isSolvable
+ extend_weight
+ instance : CanLift (Submodule R M) (LieSubmodule R L M) (·)
+ lie_stable

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).

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Jan 3, 2025
@jcommelin jcommelin changed the base branch from master to lwhitfield-Lie-theorem January 3, 2025 15:25
@jcommelin jcommelin marked this pull request as ready for review January 3, 2025 15:29
@jcommelin jcommelin merged commit 852664c into lwhitfield-Lie-theorem Jan 3, 2025
@mathlib-bors mathlib-bors bot deleted the jmc-lie-theorem-diff branch January 3, 2025 15:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant