Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-20 01:35 d12bbc00

View on Github →

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))

Estimated changes

Modified src/data/fintype.lean

Modified src/data/nat/totient.lean

added theorem nat.totient_zero

added theorem zmod.card_units_eq_totient

Modified src/data/zmod/basic.lean

added theorem zmod.cast_unit_of_coprime

added def zmod.unit_of_coprime

Modified src/data/zmod/quadratic_reciprocity.lean

Modified src/field_theory/finite.lean

added theorem nat.modeq.pow_totient

added theorem zmod.pow_totient