Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-10 17:41 03d906cb

View on Github →

feat(field_theory/finite/basic): zmod.pow_totient is true for zero (#15771)

Estimated changes

modified theorem zmod.pow_totient