-
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/nat,int): move field-specific lemmas about cast #14890
Conversation
d50bf4f
to
0d8ea09
Compare
This PR/issue depends on: |
I want to refer to the rational numbers in the definition of a field, meaning we can't have `algebra.field.basic` in the transitive imports of `data.rat.basic`. This is the first step in rearranging those imports: remove the definition of a field from the dependencies of the casts `ℕ → α` and `ℤ → α`, where `α` is a (semi)ring.
d1c359f
to
f74cc75
Compare
Any reason to merge |
These lemmas were in #14849 split off from src/algebra/group_power/lemmas.lean and src/algebra/group_with_zero/power.lean. In that PR @eric-wieser suggested that they could be merged here when the dependencies have been readjusted. |
Thanks! bors merge |
I want to refer to the rational numbers in the definition of a field, meaning we can't have `algebra.field.basic` in the transitive imports of `data.rat.basic`. This is a step in rearranging those imports: remove the definition of a field from the dependencies of the casts `ℕ → α` and `ℤ → α`, where `α` is a (semi)ring.
Pull request successfully merged into master. Build succeeded: |
In #14894, I want to refer to the rational numbers in the definition of a field, meaning we can't have `algebra.field.basic` in the transitive imports of `data.rat.basic`. Apparently this dependency was re-added, so I'm going to have to split it again...
In #14894, I want to refer to the rational numbers in the definition of a field, meaning we can't have `algebra.field.basic` in the transitive imports of `data.rat.defs`. Apparently this dependency was re-added, so I'm going to have to split it again...
In #14894, I want to refer to the rational numbers in the definition of a field, meaning we can't have `algebra.field.basic` in the transitive imports of `data.rat.defs`. Apparently this dependency was re-added, so I'm going to have to split it again...
In #14894, I want to refer to the rational numbers in the definition of a field, meaning we can't have `algebra.field.basic` in the transitive imports of `data.rat.defs`. Apparently this dependency was re-added, so I'm going to have to split it again...
I want to refer to the rational numbers in the definition of a field, meaning we can't have
algebra.field.basic
in the transitive imports ofdata.rat.basic
.This is a step in rearranging those imports: remove the definition of a field from the dependencies of the casts
ℕ → α
andℤ → α
, whereα
is a (semi)ring.