Skip to content

[Merged by Bors] - doc(GroupTheory): fix file refs#33305

Closed
harahu wants to merge 2 commits intoleanprover-community:masterfrom
harahu:doc/fix-file-refs-gt
Closed

[Merged by Bors] - doc(GroupTheory): fix file refs#33305
harahu wants to merge 2 commits intoleanprover-community:masterfrom
harahu:doc/fix-file-refs-gt

Conversation

@harahu
Copy link
Copy Markdown
Contributor

@harahu harahu commented Dec 26, 2025

Fix some stale documentation file refs.


Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions Bot commented Dec 26, 2025

PR summary 51192f7a45

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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-group-theory Group theory label Dec 26, 2025
@harahu harahu force-pushed the doc/fix-file-refs-gt branch from d55adf5 to e1d3487 Compare December 26, 2025 12:34
@harahu harahu marked this pull request as ready for review December 26, 2025 12:45
Copy link
Copy Markdown
Contributor

@bryangingechen bryangingechen left a comment

Choose a reason for hiding this comment

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

Thanks!
bors r+

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Dec 26, 2025
@bryangingechen
Copy link
Copy Markdown
Contributor

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors Bot commented Dec 26, 2025

✌️ harahu can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors Bot commented Dec 26, 2025

Canceled.

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed ready-to-merge This PR has been sent to bors. delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). labels Dec 26, 2025
@bryangingechen bryangingechen added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Dec 26, 2025
@harahu
Copy link
Copy Markdown
Contributor Author

harahu commented Dec 27, 2025

bors r+

mathlib-bors Bot pushed a commit that referenced this pull request Dec 27, 2025
Fix some stale documentation file refs.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors Bot commented Dec 27, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title doc(GroupTheory): fix file refs [Merged by Bors] - doc(GroupTheory): fix file refs Dec 27, 2025
@mathlib-bors mathlib-bors Bot closed this Dec 27, 2025
kim-em pushed a commit to kim-em/mathlib4 that referenced this pull request Jan 6, 2026
goliath-klein pushed a commit to PrParadoxy/mathlib4 that referenced this pull request Jan 24, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-group-theory Group theory

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants