-
Notifications
You must be signed in to change notification settings - Fork 251
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.
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
[Merged by Bors] - feat: generalize DirectSum
results to avoid negation
#10828
Conversation
The compilation of |
So I could make it work, but this is strange.
I found it using |
!bench |
Here are the benchmark results for commit eeeb6c8. |
@riccardobrasca , can you launch |
!bench |
I think anyone can do it (but I am not sure) |
(I tried, and nothing happened… apparently, one needs admin privileges…) |
Here are the benchmark results for commit b7dd119. Benchmark Metric Change
======================================================================
+ ~Mathlib.LinearAlgebra.DirectSum.Finsupp instructions -45.8%
+ ~Mathlib.LinearAlgebra.DirectSum.TensorProduct instructions -42.3% |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors merge
Thanks!
Three files are modified, where the hypotheses are relaxed from `Ring` or `CommRing` to `Semiring` or `CommSemiring`, and `AddCommGroup` to `AddCommMonoid`. Besides this, no definition is changed, and for one proof in `RingTheory.Flat.Basic`, I needed to add an instance (`letI`…) in the proof. (Everything pertains to direct sums of modules.) Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
DirectSum
results to avoid negation
Pull request successfully merged into master. Build succeeded: |
DirectSum
results to avoid negationDirectSum
results to avoid negation
Three files are modified, where the hypotheses are relaxed from `Ring` or `CommRing` to `Semiring` or `CommSemiring`, and `AddCommGroup` to `AddCommMonoid`. Besides this, no definition is changed, and for one proof in `RingTheory.Flat.Basic`, I needed to add an instance (`letI`…) in the proof. (Everything pertains to direct sums of modules.) Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Generalize `Basis.tensorProduct` and `instance Module.Free.tensor` to CommSemiring and AddCommMonoid Plus style fixes: * tidy up LinearAlgebra.DirectSum.Finsupp.lean: * delete unused `universe` declaration * delete duplicate `open TensorProduct` * delete redundant `noncomputable` annotation and associated comment * replace `open Classical` with `DecidableEq` type class implicit arguments * add `DecidableEq` elsewhere when needed as a result * use `variable` * delete "typeclass reminders" in "Module.Flat.iff_rTensor_injective'" (no longer needed) * whitespace fixes * simplify file structure (`section`/`namespace`/`open`/`variable`)
Generalize `Basis.tensorProduct` and `instance Module.Free.tensor` to CommSemiring and AddCommMonoid Plus style fixes: * tidy up LinearAlgebra.DirectSum.Finsupp.lean: * delete unused `universe` declaration * delete duplicate `open TensorProduct` * delete redundant `noncomputable` annotation and associated comment * replace `open Classical` with `DecidableEq` type class implicit arguments * add `DecidableEq` elsewhere when needed as a result * use `variable` * delete "typeclass reminders" in "Module.Flat.iff_rTensor_injective'" (no longer needed) * whitespace fixes * simplify file structure (`section`/`namespace`/`open`/`variable`)
Generalize `Basis.tensorProduct` and `instance Module.Free.tensor` to CommSemiring and AddCommMonoid, as a follow-up to #10828. Plus style fixes: * tidy up LinearAlgebra.DirectSum.Finsupp.lean: * delete unused `universe` declaration * delete duplicate `open TensorProduct` * delete redundant `noncomputable` annotation and associated comment (due to `noncomputable section` in the same file) * use `variable` * delete "typeclass reminders" in "Module.Flat.iff_rTensor_injective'" (no longer needed) * whitespace fixes * simplify file structure (`section`/`namespace`/`open`/`variable`) Co-authored-by: Richard Copley <rcopley@gmail.com>
Three files are modified, where the hypotheses are relaxed from `Ring` or `CommRing` to `Semiring` or `CommSemiring`, and `AddCommGroup` to `AddCommMonoid`. Besides this, no definition is changed, and for one proof in `RingTheory.Flat.Basic`, I needed to add an instance (`letI`…) in the proof. (Everything pertains to direct sums of modules.) Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Three files are modified, where the hypotheses are relaxed from `Ring` or `CommRing` to `Semiring` or `CommSemiring`, and `AddCommGroup` to `AddCommMonoid`. Besides this, no definition is changed, and for one proof in `RingTheory.Flat.Basic`, I needed to add an instance (`letI`…) in the proof. (Everything pertains to direct sums of modules.) Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Generalize `Basis.tensorProduct` and `instance Module.Free.tensor` to CommSemiring and AddCommMonoid, as a follow-up to #10828. Plus style fixes: * tidy up LinearAlgebra.DirectSum.Finsupp.lean: * delete unused `universe` declaration * delete duplicate `open TensorProduct` * delete redundant `noncomputable` annotation and associated comment (due to `noncomputable section` in the same file) * use `variable` * delete "typeclass reminders" in "Module.Flat.iff_rTensor_injective'" (no longer needed) * whitespace fixes * simplify file structure (`section`/`namespace`/`open`/`variable`) Co-authored-by: Richard Copley <rcopley@gmail.com>
Three files are modified, where the hypotheses are relaxed from `Ring` or `CommRing` to `Semiring` or `CommSemiring`, and `AddCommGroup` to `AddCommMonoid`. Besides this, no definition is changed, and for one proof in `RingTheory.Flat.Basic`, I needed to add an instance (`letI`…) in the proof. (Everything pertains to direct sums of modules.) Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Generalize `Basis.tensorProduct` and `instance Module.Free.tensor` to CommSemiring and AddCommMonoid, as a follow-up to #10828. Plus style fixes: * tidy up LinearAlgebra.DirectSum.Finsupp.lean: * delete unused `universe` declaration * delete duplicate `open TensorProduct` * delete redundant `noncomputable` annotation and associated comment (due to `noncomputable section` in the same file) * use `variable` * delete "typeclass reminders" in "Module.Flat.iff_rTensor_injective'" (no longer needed) * whitespace fixes * simplify file structure (`section`/`namespace`/`open`/`variable`) Co-authored-by: Richard Copley <rcopley@gmail.com>
Three files are modified, where the hypotheses are relaxed from `Ring` or `CommRing` to `Semiring` or `CommSemiring`, and `AddCommGroup` to `AddCommMonoid`. Besides this, no definition is changed, and for one proof in `RingTheory.Flat.Basic`, I needed to add an instance (`letI`…) in the proof. (Everything pertains to direct sums of modules.) Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Generalize `Basis.tensorProduct` and `instance Module.Free.tensor` to CommSemiring and AddCommMonoid, as a follow-up to #10828. Plus style fixes: * tidy up LinearAlgebra.DirectSum.Finsupp.lean: * delete unused `universe` declaration * delete duplicate `open TensorProduct` * delete redundant `noncomputable` annotation and associated comment (due to `noncomputable section` in the same file) * use `variable` * delete "typeclass reminders" in "Module.Flat.iff_rTensor_injective'" (no longer needed) * whitespace fixes * simplify file structure (`section`/`namespace`/`open`/`variable`) Co-authored-by: Richard Copley <rcopley@gmail.com>
Three files are modified, where the hypotheses are relaxed from
Ring
orCommRing
toSemiring
orCommSemiring
, andAddCommGroup
toAddCommMonoid
.Besides this, no definition is changed, and for one proof in
RingTheory.Flat.Basic
, I needed to add an instance (letI
…) in the proof.(Everything pertains to direct sums of modules.)