Skip to content

[Merged by Bors] - chore(Analysis/SpecialFunctions/Log/PosLog): fix non-terminal simp#39564

Closed
kebekus wants to merge 2 commits into
leanprover-community:masterfrom
kebekus:kebekus/posLog.1
Closed

[Merged by Bors] - chore(Analysis/SpecialFunctions/Log/PosLog): fix non-terminal simp#39564
kebekus wants to merge 2 commits into
leanprover-community:masterfrom
kebekus:kebekus/posLog.1

Conversation

@kebekus

@kebekus kebekus commented May 19, 2026

Copy link
Copy Markdown
Collaborator

Fix a non-terminal simp.


Open in Gitpod

@kebekus kebekus added the easy < 20s of review time. See the lifecycle page for guidelines. label May 19, 2026
@github-actions

github-actions Bot commented May 19, 2026

Copy link
Copy Markdown

PR summary 632e3075c5

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
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.


No changes to strong technical debt.
No changes to weak technical debt.

@github-actions github-actions Bot added the t-analysis Analysis (normed *, calculus) label May 19, 2026
@kebekus
kebekus marked this pull request as ready for review May 19, 2026 08:31
Comment thread Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean Outdated
Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
@themathqueen themathqueen changed the title chore: fix non-terminal simp chore(Analysis/SpecialFunctions/Log/PosLog): fix non-terminal simp May 19, 2026
@themathqueen

Copy link
Copy Markdown
Collaborator

Thanks!

maintainer merge

@github-actions

Copy link
Copy Markdown

🚀 Pull request has been placed on the maintainer queue by themathqueen.

@mathlib-triage mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 19, 2026
@faenuccio

Copy link
Copy Markdown
Contributor

Thanks!

bors merge

@mathlib-triage mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label May 19, 2026
mathlib-bors Bot pushed a commit that referenced this pull request May 19, 2026
@mathlib-triage mathlib-triage Bot removed the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 19, 2026
@mathlib-bors

mathlib-bors Bot commented May 19, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title chore(Analysis/SpecialFunctions/Log/PosLog): fix non-terminal simp [Merged by Bors] - chore(Analysis/SpecialFunctions/Log/PosLog): fix non-terminal simp May 19, 2026
@mathlib-bors mathlib-bors Bot closed this May 19, 2026
RaggedR pushed a commit to RaggedR/mathlib4 that referenced this pull request May 22, 2026
b-mehta pushed a commit to b-mehta/mathlib4 that referenced this pull request Jun 2, 2026
Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants