Skip to content

chore(NumberTheory/NumberField/InfinitePlace/Basic): add abbrev of LiesOver for InfinitePlace#41747

Open
tb65536 wants to merge 1 commit into
leanprover-community:masterfrom
tb65536:tb_lo39c
Open

chore(NumberTheory/NumberField/InfinitePlace/Basic): add abbrev of LiesOver for InfinitePlace#41747
tb65536 wants to merge 1 commit into
leanprover-community:masterfrom
tb65536:tb_lo39c

Conversation

@tb65536

@tb65536 tb65536 commented Jul 14, 2026

Copy link
Copy Markdown
Contributor

This PR adds an abbrev of LiesOver for InfinitePlace.


Open in Gitpod

@tb65536 tb65536 added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-number-theory Number theory (also use t-algebra or t-analysis to specialize) t-algebra Algebra (groups, rings, fields, etc) labels Jul 14, 2026
@github-actions

Copy link
Copy Markdown

PR summary 638521775e

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff (regex)

+ LiesOver

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

Computed after the build finishes.


No changes to strong technical debt.

No changes to weak technical debt.

Current commit 638521775e
Reference commit 383070160f

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

@ocfnash

ocfnash commented Jul 14, 2026

Copy link
Copy Markdown
Contributor

Thanks!

bors d+

@mathlib-bors mathlib-bors Bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jul 14, 2026
@mathlib-bors

mathlib-bors Bot commented Jul 14, 2026

Copy link
Copy Markdown
Contributor

✌️ tb65536 can now approve this pull request until 2026-07-28 19:14 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-algebra Algebra (groups, rings, fields, etc) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants