mathlib3
d12bbc00 - feat(data/zmod): lemmas about totient and zmod (#2158)

Commit
5 years ago
feat(data/zmod): lemmas about totient and zmod (#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>
Author
Parents
Loading