src/HOL/Algebra/Multiplicative_Group.thy
changeset 69785 9e326f6f8a24
parent 69749 10e48c47a549
child 69895 6b03a8cf092d
     1.1 --- a/src/HOL/Algebra/Multiplicative_Group.thy	Sat Feb 02 15:52:14 2019 +0100
     1.2 +++ b/src/HOL/Algebra/Multiplicative_Group.thy	Mon Feb 04 12:16:03 2019 +0100
     1.3 @@ -136,7 +136,9 @@
     1.4   shows "n > 0 \<and> n \<le> p"
     1.5   using assms by (simp add: dvd_pos_nat dvd_imp_le)
     1.6  
     1.7 -(* Deviates from the definition given in the library in number theory *)
     1.8 +(* TODO FIXME: This is the "totient" function from HOL-Number_Theory, but since part of
     1.9 +   HOL-Number_Theory depends on HOL-Algebra.Multiplicative_Group, there would be a cyclic
    1.10 +   dependency. *)
    1.11  definition phi' :: "nat => nat"
    1.12    where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m}"
    1.13