Theorem Even.eq_of_totient_eq_totient

Modification history

2025-12-16 10:54
Mathlib/Data/Nat/Totient.lean
feat(Cyclotomic): compute the torsion order of a cyclotomic field (#32782) …
Added Even.eq_of_totient_eq_totientView on Github →