Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

chore: adaptations for nightly-2024-02-26 #10995

Merged
merged 52 commits into from Feb 28, 2024
Merged

chore: adaptations for nightly-2024-02-26 #10995

merged 52 commits into from Feb 28, 2024

Conversation

semorrison
Copy link
Contributor

No description provided.

@semorrison semorrison changed the base branch from bump/v4.7.0 to master February 27, 2024 04:22
@semorrison semorrison changed the base branch from master to bump/v4.7.0 February 27, 2024 04:23
semorrison added a commit that referenced this pull request Feb 27, 2024
@semorrison
chore: more backport of simp changes from #10995
0cba88b
mathlib-bors bot pushed a commit that referenced this pull request Feb 27, 2024
@semorrison @PatrickMassot
chore: more backporting of simp changes from #10995 (#11001)
d9589c1 
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
semorrison
semorrison commented Feb 28, 2024
View reviewed changes
test/FBinop.lean Outdated Show resolved Hide resolved
mattrobball
mattrobball reviewed Feb 28, 2024
View reviewed changes
Mathlib/Algebra/GroupWithZero/Units/Basic.lean Outdated Show resolved Hide resolved
Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean Outdated Show resolved Hide resolved
Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean Outdated Show resolved Hide resolved
Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean Show resolved Hide resolved
Mathlib/Algebra/Order/Ring/Defs.lean Show resolved Hide resolved
Mathlib/CategoryTheory/Category/Basic.lean Show resolved Hide resolved
Mathlib/CategoryTheory/GradedObject/Trifunctor.lean Show resolved Hide resolved
Mathlib/Data/Erased.lean Show resolved Hide resolved
Mathlib/Data/Fintype/Order.lean Show resolved Hide resolved
Mathlib/RingTheory/Polynomial/ScaleRoots.lean
@@ -227,10 +227,12 @@ lemma add_scaleRoots_of_natDegree_eq (p q : R[X]) (r : R) (h : natDegree p = nat
r ^ (natDegree p - natDegree (p + q)) • (p + q).scaleRoots r =
p.scaleRoots r + q.scaleRoots r := by
ext n; simp only [coeff_smul, coeff_scaleRoots, coeff_add, smul_eq_mul,
mul_comm (r ^ _), mul_assoc, ← pow_add, ← h, ← add_mul, add_comm (_ - n)]
mul_comm (r ^ _), ← pow_add, ← h, ← add_mul, add_comm (_ - n)]
rw [mul_assoc, ← pow_add]
Copy link
Collaborator

Choose a reason for hiding this comment

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

Why do these not fire in simp now?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

They do fire, but mul_assoc induces a max rec depth error.

I've added an "adaptation note" explaining this, but am inclined to ship.

mattrobball
mattrobball approved these changes Feb 28, 2024
View reviewed changes
Copy link
Collaborator

@mattrobball mattrobball left a comment

Choose a reason for hiding this comment

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

Good with me

@kmill kmill merged commit b700984 into bump/v4.7.0 Feb 28, 2024
15 of 16 checks passed
@mathlib-bors mathlib-bors bot deleted the bump/nightly-2024-02-26 branch February 28, 2024 05:08
riccardobrasca pushed a commit that referenced this pull request Mar 1, 2024
@semorrison @PatrickMassot @riccardobrasca
chore: more backporting of simp changes from #10995 (#11001)
052bc52 
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
kbuzzard pushed a commit that referenced this pull request Mar 12, 2024
@semorrison @PatrickMassot @kbuzzard
chore: more backporting of simp changes from #10995 (#11001)
7fd0498 
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@semorrison @PatrickMassot @dagurtomas
chore: more backporting of simp changes from #10995 (#11001)
66c0098 
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Louddy pushed a commit that referenced this pull request Apr 15, 2024
@semorrison @PatrickMassot @Louddy
chore: more backporting of simp changes from #10995 (#11001)
fbfd450 
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kmill kmill kmill approved these changes

@mattrobball mattrobball mattrobball approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@semorrison @kmill @mattrobball @Ruben-VandeVelde @Vierkantor