Skip to content

chore(Analysis/Meromorphic/Order): fix defeq abuse#41392

Open
themathqueen wants to merge 3 commits into
leanprover-community:masterfrom
themathqueen:fix_defeqabuse_meromorphicOrder
Open

chore(Analysis/Meromorphic/Order): fix defeq abuse#41392
themathqueen wants to merge 3 commits into
leanprover-community:masterfrom
themathqueen:fix_defeqabuse_meromorphicOrder

Conversation

@themathqueen

Copy link
Copy Markdown
Collaborator

Remove defeq abuse via Option.ne_none_iff_exists'.


Open in Gitpod

@themathqueen themathqueen added easy < 20s of review time. See the lifecycle page for guidelines. t-analysis Analysis (normed *, calculus) labels Jul 5, 2026
@github-actions

github-actions Bot commented Jul 5, 2026

Copy link
Copy Markdown

PR summary 7435c41fb1

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff (regex)

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.

Declarations diff (Lean)

Lean-aware diff — post-build, computed from the Lean environment (commit 7435c41).

  • +0 new declarations
  • −0 removed declarations

No declaration differences.


No changes to strong technical debt.

No changes to weak technical debt.

Current commit 7435c41fb1
Reference commit f682f8f0e2

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

Comment thread Mathlib/Analysis/Meromorphic/Order.lean Outdated
Comment thread Mathlib/Analysis/Meromorphic/Order.lean Outdated
@loefflerd loefflerd changed the title chore(Analysis/Mermorphic/Order): fix defeq abuse chore(Analysis/Meromorphic/Order): fix defeq abuse Jul 5, 2026
Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
@loefflerd loefflerd requested a review from kebekus July 5, 2026 20:41

@kebekus kebekus left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

The changes suggested here look good to me. Thanks!

@loefflerd

Copy link
Copy Markdown
Contributor

maintainer merge

@github-actions

github-actions Bot commented Jul 6, 2026

Copy link
Copy Markdown

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

@mathlib-triage mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 6, 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. maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-analysis Analysis (normed *, calculus)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants