Commit 2023-03-29 05:37 27f57693

View on Github →

feat: port Data.Nat.Totient (#3156)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Totient.lean

added theorem Nat.Ico_filter_coprime_le

added theorem Nat.card_units_zMod_lt_sub_one

added theorem Nat.filter_coprime_Ico_eq_totient

added theorem Nat.prime_iff_card_units

added theorem Nat.sum_totient'

added theorem Nat.sum_totient

added def Nat.totient

added theorem Nat.totient_div_of_dvd

added theorem Nat.totient_dvd_of_dvd

added theorem Nat.totient_eq_card_coprime

added theorem Nat.totient_eq_card_lt_and_coprime

added theorem Nat.totient_eq_div_factors_mul

added theorem Nat.totient_eq_iff_prime

added theorem Nat.totient_eq_mul_prod_factors

added theorem Nat.totient_eq_one_iff

added theorem Nat.totient_eq_prod_factorization

added theorem Nat.totient_even

added theorem Nat.totient_gcd_mul_totient_mul

added theorem Nat.totient_le

added theorem Nat.totient_lt

added theorem Nat.totient_mul

added theorem Nat.totient_mul_of_prime_of_dvd

added theorem Nat.totient_mul_of_prime_of_not_dvd

added theorem Nat.totient_mul_prod_factors

added theorem Nat.totient_one

added theorem Nat.totient_pos

added theorem Nat.totient_prime

added theorem Nat.totient_prime_pow

added theorem Nat.totient_prime_pow_succ

added theorem Nat.totient_super_multiplicative

added theorem Nat.totient_two

added theorem Nat.totient_zero

added theorem ZMod.card_units_eq_totient