Commit 2024-05-06 04:08 34323947

View on Github →

feat: add Nat.totient_eq_zero (#12685) Also upgrade totient_pos to an iff.

Estimated changes

Modified Mathlib/Data/Nat/Totient.lean

added theorem Nat.totient_eq_zero

modified theorem Nat.totient_one

modified theorem Nat.totient_pos

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

Modified Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean

Modified Mathlib/Topology/Instances/AddCircle.lean