equal
deleted
inserted
replaced
380 qed |
380 qed |
381 |
381 |
382 (* Euler totient function. *) |
382 (* Euler totient function. *) |
383 |
383 |
384 definition phi_def: "\<phi> n = card { m. 0 < m \<and> m <= n \<and> coprime m n }" |
384 definition phi_def: "\<phi> n = card { m. 0 < m \<and> m <= n \<and> coprime m n }" |
|
385 |
385 lemma phi_0[simp]: "\<phi> 0 = 0" |
386 lemma phi_0[simp]: "\<phi> 0 = 0" |
386 unfolding phi_def by (auto simp add: card_eq_0_iff) |
387 unfolding phi_def by auto |
387 |
388 |
388 lemma phi_finite[simp]: "finite ({ m. 0 < m \<and> m <= n \<and> coprime m n })" |
389 lemma phi_finite[simp]: "finite ({ m. 0 < m \<and> m <= n \<and> coprime m n })" |
389 proof- |
390 proof- |
390 have "{ m. 0 < m \<and> m <= n \<and> coprime m n } \<subseteq> {0..n}" by auto |
391 have "{ m. 0 < m \<and> m <= n \<and> coprime m n } \<subseteq> {0..n}" by auto |
391 thus ?thesis by (auto intro: finite_subset) |
392 thus ?thesis by (auto intro: finite_subset) |