Skip to content

[Merged by Bors] - chore(Mathlib/Algebra/Lie/Subalgebra.lean): automated extraction#37203

Closed
mathlib-splicebot[bot] wants to merge 1 commit intomasterfrom
splice-bot/pr-34727-Mathlib-Algebra-Lie-Subalgebra.lean-ead4585ef0-czusarp
Closed

[Merged by Bors] - chore(Mathlib/Algebra/Lie/Subalgebra.lean): automated extraction#37203
mathlib-splicebot[bot] wants to merge 1 commit intomasterfrom
splice-bot/pr-34727-Mathlib-Algebra-Lie-Subalgebra.lean-ead4585ef0-czusarp

Conversation

@mathlib-splicebot
Copy link
Contributor

This PR was automatically created from PR #34727 by @ocfnash via a review comment by @jcommelin.

@jcommelin jcommelin added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Mar 26, 2026
@github-actions
Copy link

PR summary 9445d1c3b0

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ comap_lieSpan_range_eq
+ lieSpan_lieSpan_coe_preimage

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

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

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


No changes to technical debt.

You can run this locally as

./scripts/reporting/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 Mar 26, 2026
@mathlib-auto-merge
Copy link

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Mar 26, 2026
)

This PR was automatically created from PR #34727 by @ocfnash via a [review comment](#34727 (comment)) by @jcommelin.

Co-authored-by: ocfnash <7734364+ocfnash@users.noreply.github.com>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Mar 26, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Mathlib/Algebra/Lie/Subalgebra.lean): automated extraction [Merged by Bors] - chore(Mathlib/Algebra/Lie/Subalgebra.lean): automated extraction Mar 26, 2026
@mathlib-bors mathlib-bors bot closed this Mar 26, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants