Theorem zmod.card_units_eq_totient
Modification history
2022-08-29 20:00
src/data/nat/totient.lean
feat(*): replace fact(0 < t) with ne_zero (#16145) …
Modified zmod.card_units_eq_totientView on Github →2022-06-20 16:13
src/data/nat/totient.lean
chore(data/nat/totient): golf a proof (#14851)
Modified zmod.card_units_eq_totientView on Github →2022-01-05 23:45
src/data/nat/totient.lean
chore(*): notation for `units` (#11236)
Modified zmod.card_units_eq_totientView on Github →2021-11-05 00:43
src/data/nat/totient.lean
feat(number_theory/lucas_primality): Add theorem for Lucas primality test (#8820) …
Modified zmod.card_units_eq_totientView on Github →2021-07-27 23:02
src/data/nat/totient.lean
feat(data/nat/totient): totient_mul (#8441) …
Modified zmod.card_units_eq_totientView on Github →