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] - chore(Data/Finsupp/Defs): rename instances #10976
Conversation
This adds the `inst` prefix that is expected in Lean 4. All the changes to downstream files are fallout, no names have been changed there.
@@ -1456,7 +1456,7 @@ instance nonUnitalCommSemiring [CommSemiring k] [AddCommSemigroup G] : | |||
#align add_monoid_algebra.non_unital_comm_semiring AddMonoidAlgebra.nonUnitalCommSemiring | |||
|
|||
instance nontrivial [Semiring k] [Nontrivial k] [Nonempty G] : Nontrivial k[G] := |
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.
Renaming these instance can come in a later PR.
maintainer merge I don't think aliases are needed for instances |
🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde. |
Thanks! 🎉 |
Thanks! bors merge |
Already running a review |
This adds the `inst` prefix that is expected in Lean 4. Performed using the F2 shortcut (renaming `foo` to `Finsupp.instFoo`, then deleting the redundant `Finsupp`) All the changes to downstream files are fallout, no names have been changed there.
Build failed (retrying...): |
This adds the `inst` prefix that is expected in Lean 4. Performed using the F2 shortcut (renaming `foo` to `Finsupp.instFoo`, then deleting the redundant `Finsupp`) All the changes to downstream files are fallout, no names have been changed there.
Pull request successfully merged into master. Build succeeded: |
This adds the `inst` prefix that is expected in Lean 4. Performed using the F2 shortcut (renaming `foo` to `Finsupp.instFoo`, then deleting the redundant `Finsupp`) All the changes to downstream files are fallout, no names have been changed there.
This adds the `inst` prefix that is expected in Lean 4. Performed using the F2 shortcut (renaming `foo` to `Finsupp.instFoo`, then deleting the redundant `Finsupp`) All the changes to downstream files are fallout, no names have been changed there.
This adds the `inst` prefix that is expected in Lean 4. Performed using the F2 shortcut (renaming `foo` to `Finsupp.instFoo`, then deleting the redundant `Finsupp`) All the changes to downstream files are fallout, no names have been changed there.
This adds the `inst` prefix that is expected in Lean 4. Performed using the F2 shortcut (renaming `foo` to `Finsupp.instFoo`, then deleting the redundant `Finsupp`) All the changes to downstream files are fallout, no names have been changed there.
This adds the
inst
prefix that is expected in Lean 4.Performed using the F2 shortcut (renaming
foo
toFinsupp.instFoo
, then deleting the redundantFinsupp
)All the changes to downstream files are fallout, no names have been changed there.