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(data/zmod/basic): Explicitly state computable right_inverses instead of just surjectivity #5797
Conversation
eric-wieser
commented
Jan 18, 2021
src/data/zmod/basic.lean
Outdated
@@ -219,36 +219,36 @@ by { cases n; refl } | |||
|
|||
end | |||
|
|||
lemma nat_cast_surjective [fact (0 < n)] : | |||
function.surjective (coe : ℕ → zmod n) := | |||
lemma nat_cast_right_inverse [fact (0 < n)] : |
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 name sounds like nat_cast
is the right inverse...
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.
I don't know what the naming convention is for these... I can currently find these lemmas that seem to match what I think you would suggest:
right_inverse_pth_root_frobenius
prod.swap_right_inverse
equiv.right_inverse_symm
Along with the lemmas that I added recently, which seem to match what I've done here:
free_algebra.algebra_map_left_inverse
tensor_algebra.ι_left_inverse
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.
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.
Can we say that this is blocked on #5829, and then come back to it when that is resolved either way?
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.
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.
I still think that the names used in this PR are confusing. If that issue can be solved, this PR is ready for merging.
…mes (#6280) Split from #5797. This takes the new proofs without introducing the objectionable names. This also renames a bunch of lemmas from `zmod.cast_*` to `zmod.nat_cast_*` and `zmod.int_cast_*`, in order to distinguish lemmas about `zmod.cast` from lemmas about `nat.cast` and `int.cast` applied with a zmod argument. As an example, `zmod.cast_val` has been renamed to `zmod.nat_cast_zmod_val`, as the lemma statement is defeq to `(nat.cast : ℕ → zmod n) (zmod.val x) = x`, and `zmod.nat_cast_val` is already taken by `nat.cast (zmod.val x) = (x : R)`. The full list of renames: * `zmod.cast_val` → `zmod.nat_cast_zmod_val` * `zmod.cast_self` → `zmod.nat_cast_self` * `zmod.cast_self'` → `zmod.nat_cast_self'` * `zmod.cast_mod_nat` → `zmod.nat_cast_mod` * `zmod.cast_mod_int` → `zmod.int_cast_mod` * `zmod.val_cast_nat` → `zmod.val_nat_cast` * `zmod.coe_to_nat` → `zmod.nat_cast_to_nat` * `zmod.cast_unit_of_coprime` → `coe_unit_of_coprime` * `zmod.cast_nat_abs_val_min_abs` → `zmod.nat_cast_nat_abs_val_min_abs`
…mes (#6280) Split from #5797. This takes the new proofs without introducing the objectionable names. This also renames a bunch of lemmas from `zmod.cast_*` to `zmod.nat_cast_*` and `zmod.int_cast_*`, in order to distinguish lemmas about `zmod.cast` from lemmas about `nat.cast` and `int.cast` applied with a zmod argument. As an example, `zmod.cast_val` has been renamed to `zmod.nat_cast_zmod_val`, as the lemma statement is defeq to `(nat.cast : ℕ → zmod n) (zmod.val x) = x`, and `zmod.nat_cast_val` is already taken by `nat.cast (zmod.val x) = (x : R)`. The full list of renames: * `zmod.cast_val` → `zmod.nat_cast_zmod_val` * `zmod.cast_self` → `zmod.nat_cast_self` * `zmod.cast_self'` → `zmod.nat_cast_self'` * `zmod.cast_mod_nat` → `zmod.nat_cast_mod` * `zmod.cast_mod_int` → `zmod.int_cast_mod` * `zmod.val_cast_nat` → `zmod.val_nat_cast` * `zmod.coe_to_nat` → `zmod.nat_cast_to_nat` * `zmod.cast_unit_of_coprime` → `coe_unit_of_coprime` * `zmod.cast_nat_abs_val_min_abs` → `zmod.nat_cast_nat_abs_val_min_abs`
c32a8af
to
24cdd4f
Compare
…tead of just surjectivity
24cdd4f
to
026b3b5
Compare
I've updated this PR now that #6280 is merged, so that now it contains no changes other than new lemma statements |
Since the Zulip discussion has been inactive for a while without resolution, I think you should do whatever you feel is best and when someone later has a good idea to fix it, they can go ahead and implement it. (That person might turn out to be me, but no promises.) |
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.
I'll put this on the queue now. These lemmas look useful and we can always change the names later.
bors r+
…tead of just surjectivity (#5797)
Pull request successfully merged into master. Build succeeded: |
…mes (#6280) Split from #5797. This takes the new proofs without introducing the objectionable names. This also renames a bunch of lemmas from `zmod.cast_*` to `zmod.nat_cast_*` and `zmod.int_cast_*`, in order to distinguish lemmas about `zmod.cast` from lemmas about `nat.cast` and `int.cast` applied with a zmod argument. As an example, `zmod.cast_val` has been renamed to `zmod.nat_cast_zmod_val`, as the lemma statement is defeq to `(nat.cast : ℕ → zmod n) (zmod.val x) = x`, and `zmod.nat_cast_val` is already taken by `nat.cast (zmod.val x) = (x : R)`. The full list of renames: * `zmod.cast_val` → `zmod.nat_cast_zmod_val` * `zmod.cast_self` → `zmod.nat_cast_self` * `zmod.cast_self'` → `zmod.nat_cast_self'` * `zmod.cast_mod_nat` → `zmod.nat_cast_mod` * `zmod.cast_mod_int` → `zmod.int_cast_mod` * `zmod.val_cast_nat` → `zmod.val_nat_cast` * `zmod.coe_to_nat` → `zmod.nat_cast_to_nat` * `zmod.cast_unit_of_coprime` → `coe_unit_of_coprime` * `zmod.cast_nat_abs_val_min_abs` → `zmod.nat_cast_nat_abs_val_min_abs`
…tead of just surjectivity (#5797)