Theorem Nat.totient_eq_card_lt_and_coprime

Modification history