src/HOL/Number_Theory/Totient.thy
changeset 69785 9e326f6f8a24
parent 69064 5840724b1d71
     1.1 --- a/src/HOL/Number_Theory/Totient.thy	Sat Feb 02 15:52:14 2019 +0100
     1.2 +++ b/src/HOL/Number_Theory/Totient.thy	Mon Feb 04 12:16:03 2019 +0100
     1.3 @@ -62,6 +62,21 @@
     1.4    shows "n - 1 \<in> totatives n"
     1.5    using assms coprime_diff_one_left_nat [of n] by (simp add: in_totatives_iff)
     1.6  
     1.7 +lemma power_in_totatives:
     1.8 +  assumes "m > 1" "coprime m g"
     1.9 +  shows   "g ^ i mod m \<in> totatives m"
    1.10 +proof -
    1.11 +  have "\<not>m dvd g ^ i"
    1.12 +  proof
    1.13 +    assume "m dvd g ^ i"
    1.14 +    hence "\<not>coprime m (g ^ i)"
    1.15 +      using \<open>m > 1\<close> by (subst coprime_absorb_left) auto
    1.16 +    with \<open>coprime m g\<close> show False by simp
    1.17 +  qed
    1.18 +  with assms show ?thesis
    1.19 +    by (auto simp: totatives_def coprime_commute intro!: Nat.gr0I)
    1.20 +qed
    1.21 +
    1.22  lemma totatives_prime_power_Suc:
    1.23    assumes "prime p"
    1.24    shows   "totatives (p ^ Suc n) = {0<..p^Suc n} - (\<lambda>m. p * m) ` {0<..p^n}"
    1.25 @@ -198,6 +213,18 @@
    1.26  lemma totient_gt_0_iff [simp]: "totient n > 0 \<longleftrightarrow> n > 0"
    1.27    by (auto intro: Nat.gr0I)
    1.28  
    1.29 +lemma totient_gt_1:
    1.30 +  assumes "n > 2"
    1.31 +  shows   "totient n > 1"
    1.32 +proof -
    1.33 +  have "{1, n - 1} \<subseteq> totatives n"
    1.34 +    using assms coprime_diff_one_left_nat[of n] by (auto simp: totatives_def)
    1.35 +  hence "card {1, n - 1} \<le> card (totatives n)"
    1.36 +    by (intro card_mono) auto
    1.37 +  thus ?thesis using assms
    1.38 +    by (simp add: totient_def)
    1.39 +qed
    1.40 +
    1.41  lemma card_gcd_eq_totient:
    1.42    "n > 0 \<Longrightarrow> d dvd n \<Longrightarrow> card {k\<in>{0<..n}. gcd k n = d} = totient (n div d)"
    1.43    unfolding totient_def by (rule sym, rule bij_betw_same_card[OF bij_betw_totatives_gcd_eq])