Skip to content

[Merged by Bors] - feat: Two lemmas on divisibility and coprimality of expand#20143

Closed
seewoo5 wants to merge 18 commits intomasterfrom
feature/expand_lemmas
Closed

[Merged by Bors] - feat: Two lemmas on divisibility and coprimality of expand#20143
seewoo5 wants to merge 18 commits intomasterfrom
feature/expand_lemmas

Conversation

@seewoo5
Copy link
Copy Markdown
Collaborator

@seewoo5 seewoo5 commented Dec 20, 2024 •
edited by YaelDillies
Loading

@seewoo5 seewoo5 added the t-algebra Algebra (groups, rings, fields, etc) label Dec 20, 2024
@seewoo5 seewoo5 self-assigned this Dec 20, 2024
@seewoo5 seewoo5 mentioned this pull request Dec 20, 2024
Closed
7 tasks
@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Dec 20, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 20, 2024 •
edited
Loading

PR summary 332197ad4a

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ contract_C
+ contract_add
+ contract_mul_expand
+ isCoprime_expand

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

@seewoo5
Copy link
Copy Markdown
Collaborator Author

seewoo5 commented Dec 20, 2024

Anyone knows why there's a build error?

✖ [5536/5789] Building Mathlib.RingTheory.Localization.Integral
trace: .> LEAN_PATH=././.lake/packages/Cli/.lake/build/lib:././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/LeanSearchClient/.lake/build/lib:././.lake/packages/plausible/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH=././.lake/build/lib:././.lake/packages/plausible/.lake/build/lib:././.lake/packages/LeanSearchClient/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:/home/lean/.elan/toolchains/leanprover--lean4---v4.15.0-rc1/lib/lean:/home/lean/.elan/toolchains/leanprover--lean4---v4.15.0-rc1/lib /home/lean/.elan/toolchains/leanprover--lean4---v4.15.0-rc1/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -Dweak.linter.docPrime=true -Dweak.linter.hashCommand=true -Dweak.linter.oldObtain=true -Dweak.linter.refine=true -Dweak.linter.style.cdot=true -Dweak.linter.style.dollarSyntax=true -Dweak.linter.style.header=true -Dweak.linter.style.lambdaSyntax=true -Dweak.linter.style.longLine=true -Dweak.linter.style.longFile=1500 -Dweak.linter.style.missingEnd=true -Dweak.linter.style.multiGoal=true -Dweak.linter.style.setOption=true ././././Mathlib/RingTheory/Localization/Integral.lean -R ./././. -o ././.lake/build/lib/Mathlib/RingTheory/Localization/Integral.olean -i ././.lake/build/lib/Mathlib/RingTheory/Localization/Integral.ilean -c ././.lake/build/ir/Mathlib/RingTheory/Localization/Integral.c --json
error: ././././Mathlib/RingTheory/Localization/Integral.lean:321:8: ambiguous, possible interpretations 
  _root_.map_eq_zero (algebraMap K L) : (algebraMap K L) ?m.157807 = 0 ↔ ?m.157807 = 0
  
  Polynomial.map_eq_zero (algebraMap K L) : Polynomial.map (algebraMap K L) ?m.158624 = 0 ↔ ?m.158624 = 0
error: Lean exited with code 1
Some required builds logged failures:
- Mathlib.RingTheory.Localization.Integral
error: build failed
Running linter on specified module: Mathlib
uncaught exception: object file '././.lake/build/lib/Mathlib.olean' of module Mathlib does not exist
Error: The process '/usr/bin/env' failed with exit code 1

@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented Dec 23, 2024

map_eq_zero is now ambiguous with Polynomial.map_eq_zero when Polynomial is open. Here I would suggest marking Polynomial.map_eq_zero as protected

YaelDillies
YaelDillies reviewed Dec 24, 2024
View reviewed changes
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 24, 2024
@seewoo5 seewoo5 mentioned this pull request Dec 27, 2024
Closed
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Dec 27, 2024
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Dec 27, 2024

This PR/issue depends on:

alreadydone
alreadydone requested changes Dec 30, 2024
View reviewed changes
@jcpaik jcpaik mentioned this pull request Dec 30, 2024
Merged
@jcpaik
Merge pull request #20343 from leanprover-community/jyxu/expand_lemmas
5291f7f 
feature/expand_lemmas <- Jyxu/expand lemmas
@github-actions github-actions bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! and removed large-import Automatically added label for PRs with a significant increase in transitive imports labels Dec 30, 2024
@jcpaik jcpaik removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 30, 2024
@jcpaik jcpaik requested a review from alreadydone December 30, 2024 15:46
alreadydone
alreadydone approved these changes Dec 30, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@alreadydone alreadydone left a comment

Choose a reason for hiding this comment

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

LGTM!
Maybe @YaelDillies could call maintainer merge?

YaelDillies
YaelDillies reviewed Dec 30, 2024
View reviewed changes
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 30, 2024
alreadydone and others added 2 commits December 30, 2024 17:37
@alreadydone
upgrade to iff
bd8328d
@alreadydone @YaelDillies
@[simp] theorem contract_C
5ef5937 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
alreadydone
alreadydone reviewed Dec 31, 2024
View reviewed changes
@alreadydone @YaelDillies
Make arguments explicit
65ef3da 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@alreadydone alreadydone added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jan 1, 2025
@jcpaik @alreadydone
Remove expand_dvd
5c73901 
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
@jcpaik jcpaik removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 3, 2025
YaelDillies
YaelDillies approved these changes Jan 3, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

Thanks!

maintainer delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 3, 2025

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 3, 2025
@jcpaik @YaelDillies
make isCoprime_expand a simp lemma
332197a 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Jan 3, 2025

Thanks!

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jan 3, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jan 3, 2025
@seewoo5 @alreadydone @jcpaik
feat: Two lemmas on divisibility and coprimality of expand (#20143)
3e65a9f 
Co-authored-by: Seewoo Lee <49933279+seewoo5@users.noreply.github.com>
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Co-authored-by: Jineon Baek <34874130+jcpaik@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 3, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Two lemmas on divisibility and coprimality of expand [Merged by Bors] - feat: Two lemmas on divisibility and coprimality of expand Jan 3, 2025
@mathlib-bors mathlib-bors bot closed this Jan 3, 2025
@mathlib-bors mathlib-bors bot deleted the feature/expand_lemmas branch January 3, 2025 14:20
Julian added a commit that referenced this pull request Jan 5, 2025
@Julian
Merge remote-tracking branch 'origin/master' into bhargava-factorial
9857da3 
* origin/master: (133 commits)
  chore(1000): remove nonexistent fields (#20493)
  chore(CategoryTheory/Adjunction.Basic, CategoryTheory/Equivalence): change definition of `Adjunction.comp` and `Equivalence.trans` (#20490)
  feat(Asymptotics): add `Asymptotics.*.*Prod` lemmas (#20458)
  feat: a conditional kernel is almost everywhere a probability measure (#20430)
  feat: if `f` is a measurable group hom, then every point has a neighborhood `s` such that `f '' s` is bounded (#20304)
  feat: `Ico`, `Ioc`, and `Ioo` are not closed or compact (#20479)
  chore: drop redundant hypothesis in `Module.Dual.eq_of_preReflection_mapsTo` (#20492)
  feat(FaaDiBruno): derive `DecidableEq` (#20482)
  chore(SetTheory/Ordinal/Basic): `{x // x < y}` → `Iio y` (#20413)
  chore: generalize `FormalMultilinearSeries.ofScalars_norm` to `Seminormed` (#20351)
  chore(MvPolynomial/Localization): golf using TensorProduct (#20309)
  chore(Combinatorics/Enumerative/Partition): auto-derive DecidableEq (#20277)
  chore(CategoryTheory): make relevant parameters explicit in `Arrow.homMk`. (#20259)
  feat: add `IsStarNormal (↑x⁻¹ : R)` instance for `x : Rˣ` (#20091)
  fix: Stop cancelling builds of master (#20435)
  chore: update Mathlib dependencies 2025-01-05 (#20485)
  feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas (#18933)
  chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0 (#20464)
  chore: bot validates lean-toolchain on bump/v4.X.0 branches (#20478)
  feat: shorthand lemmas for the L1 norm (#20383)
  chore: remove unnecessary adaptation notes (#20467)
  chore(Algebra/Category/MonCat/Colimits): remove smallness condition (#20473)
  chore(SetTheory/Ordinal/Arithmetic): `IsLeftCancelAdd Ordinal` (#19888)
  feat(Algebra): more on `OrthogonalIdempotents` (#18195)
  feat(Radical): `(radical a).natDegree ≤ a.natDegree` (#20468)
  feat(Polynomial): `(a^n)' = 0` iff `a' = 0` when `n` doesn't divide the characteristic (#20190)
  feat(Algebra/Lie): add Lie's theorem (#13480)
  chore(RingTheory/Generators): make algebra instance a def (#14265)
  feat(Topology/Group): Lemmas about profinite group (#20282)
  feat: the empty set is a topological basis iff the space is empty (#20441)
  chore: make uniqueness of conditionally complete linearly ordered archimedean fields independent of the construction of `Real` (#20242)
  chore: `inherit_doc`s for notations (#20376)
  chore: split AEEqOfIntegral into two files, one for each integral type (#20405)
  chore: split Kernel/MeasurableIntegral (#20427)
  feat(MeasureTheory/Group/Measure): add ContinuousMulEquiv.isHaarMeasure_map (#20469)
  fix(Mathlib.Tactic.CC.Datatypes): `cc` raises panic (#20422)
  feat(Probability/Moments): add lemmas about moment generating functions (#19886)
  feat(Algebra/Order/AddGroupWithTop): lemmas about LinearOrderedAddCommGroupWithTop (#18954)
  chore: bump toolchain to v4.15.0 (#20461)
  chore: update Mathlib dependencies 2025-01-04 (#20463)
  fix: make `Prod` projection delaborators respond to options, add option to disable (#20455)
  chore(Algebra): Improve attribute generation (#20451)
  feat(Polynomial): `(C a * p).degree = p.degree` if `a * p.leadingCoeff ≠ 0` (#20446)
  feat: add `ENNReal.finStronglyMeasurable_of_measurable` (#20404)
  doc(Algebra/Lie/Weights/Basic): fix typo (#20450)
  chore(1000): remove `identifiers` (#20445)
  feat: add sumPiEquivProdPi and piUnique (#20195)
  feat: add fst_compProd_apply (#20429)
  chore: use unsigned measures for Lebesgue decomposition (#20400)
  feat: Two lemmas on divisibility and coprimality of `expand` (#20143)
  ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@alreadydone alreadydone alreadydone approved these changes

@YaelDillies YaelDillies YaelDillies approved these changes

+1 more reviewer

@jcpaik jcpaik jcpaik left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

@seewoo5 seewoo5

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@seewoo5 @YaelDillies @mathlib4-dependent-issues-bot @riccardobrasca @alreadydone @jcpaik