-
Notifications
You must be signed in to change notification settings - Fork 297
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/fintype/basic): make units.fintype computable #9846
Conversation
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.
Thanks 🎉
If CI passes, please remove the label awaiting-CI
and merge this yourself, by adding a comment bors r+
.
bors d+
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
…intype # Conflicts: # src/ring_theory/integral_domain.lean
@jcommelin: fixing CI resulted in some scope creep, would you mind taking a second look? |
@eric-wieser Sure. (In such cases, I think it's best to remove |
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.
LGTM. Feel free to merge it. Unless you want to mover even more stuff around (-;
@@ -115,10 +110,13 @@ begin | |||
this, mul_one] | |||
end | |||
|
|||
section | |||
variables [group_with_zero K] [fintype K] |
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.
This suggest that it really should move to a different file. Maybe in another PR?
bors merge |
This also: * renames `equiv.units_equiv_ne_zero` to `units_equiv_ne_zero`, and resolves the TODO comment about generalization * renames and generalizes `finite_field.card_units` to `fintype.card_units`, and proves it right next to the fintype instance * generalizes some typeclass assumptions in `finite_field.basic` as the linter already required me to tweak them
bors merge |
This also: * renames `equiv.units_equiv_ne_zero` to `units_equiv_ne_zero`, and resolves the TODO comment about generalization * renames and generalizes `finite_field.card_units` to `fintype.card_units`, and proves it right next to the fintype instance * generalizes some typeclass assumptions in `finite_field.basic` as the linter already required me to tweak them
Pull request successfully merged into master. Build succeeded: |
This also: * renames `equiv.units_equiv_ne_zero` to `units_equiv_ne_zero`, and resolves the TODO comment about generalization * renames and generalizes `finite_field.card_units` to `fintype.card_units`, and proves it right next to the fintype instance * generalizes some typeclass assumptions in `finite_field.basic` as the linter already required me to tweak them
This also:
equiv.units_equiv_ne_zero
tounits_equiv_ne_zero
, and resolves the TODO comment about generalizationfinite_field.card_units
tofintype.card_units
, and proves it right next to the fintype instancefinite_field.basic
as the linter already required me to tweak them