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])
```