feat(data/zmod): lemmas about totient and zmod#2158
Conversation
|
Thanks for writing up the PR |
src/data/zmod/basic.lean
Outdated
| left_inv := λ ⟨_, _, _, _⟩, units.ext (by simp), | ||
| right_inv := λ ⟨_, _⟩, by simp } | ||
|
|
||
| instance units.fintype {n : ℕ+} : fintype (units (zmod n)) := |
There was a problem hiding this comment.
Shouldn't this be generalised? zmod n is a fintype, hence units is a fintype.
There was a problem hiding this comment.
We are moving away from constructivism by defining things in that generality, but I'm okay with that.
There was a problem hiding this comment.
Hmm, I'm certainly ok with that.
But I would expect that in a finite ring you can constructively build the fintype of units. Anyway, I don't really care.
There was a problem hiding this comment.
With a decidable_eq assumption it can be made computable by just searching for the inverse, but this is getting towards pointless computability I think, where the most general algorithm is so slow it's kind of pointless, so I just made a noncomputable instance.
jcommelin
added
the
ready-to-merge
src/data/zmod/basic.lean
Outdated
|
|
||
| instance decidable_eq : decidable_eq (zmodp p hp) := fin.decidable_eq _ | ||
|
|
||
| instance (h : prime 2) : subsingleton (units (zmodp 2 h)) := |
There was a problem hiding this comment.
Do you want to provide a similar instance for units (zmod 2)?
* feat(data/zmod): lemmas about totient and zmod * docstring * Changes based on Johan's comments * fix build * subsingleton (units(zmod 2)) Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
…2158) * feat(data/zmod): lemmas about totient and zmod * docstring * Changes based on Johan's comments * fix build * subsingleton (units(zmod 2)) Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
…2158) * feat(data/zmod): lemmas about totient and zmod * docstring * Changes based on Johan's comments * fix build * subsingleton (units(zmod 2)) Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
3 participants
The theorem
pow_totientended up infield_theory/finite, which is not quite right, since it's not about fields, but the imports were most appropriate there.TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list