|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
scenario.txt
Sprache: Isabelle
|
|
(* Title: HOL/Algebra/Multiplicative_Group.thy
Author: Simon Wimmer
Author: Lars Noschinski
*)
theory Multiplicative_Group
imports
Complex_Main
Group
Coset
UnivPoly
Generated_Groups
Elementary_Groups
begin
section \<open>Simplification Rules for Polynomials\<close>
text_raw \<open>\label{sec:simp-rules}\<close>
lemma (in ring_hom_cring) hom_sub[simp]:
assumes "x \ carrier R" "y \ carrier R"
shows "h (x \ y) = h x \\<^bsub>S\<^esub> h y"
using assms by (simp add: R.minus_eq S.minus_eq)
context UP_ring begin
lemma deg_nzero_nzero:
assumes deg_p_nzero: "deg R p \ 0"
shows "p \ \\<^bsub>P\<^esub>"
using deg_zero deg_p_nzero by auto
lemma deg_add_eq:
assumes c: "p \ carrier P" "q \ carrier P"
assumes "deg R q \ deg R p"
shows "deg R (p \\<^bsub>P\<^esub> q) = max (deg R p) (deg R q)"
proof -
let ?m = "max (deg R p) (deg R q)"
from assms have "coeff P p ?m = \ \ coeff P q ?m \ \"
by (metis deg_belowI lcoeff_nonzero[OF deg_nzero_nzero] linear max.absorb_iff2 max.absorb1)
then have "coeff P (p \\<^bsub>P\<^esub> q) ?m \ \"
using assms by auto
then have "deg R (p \\<^bsub>P\<^esub> q) \ ?m"
using assms by (blast intro: deg_belowI)
with deg_add[OF c] show ?thesis by arith
qed
lemma deg_minus_eq:
assumes "p \ carrier P" "q \ carrier P" "deg R q \ deg R p"
shows "deg R (p \\<^bsub>P\<^esub> q) = max (deg R p) (deg R q)"
using assms by (simp add: deg_add_eq a_minus_def)
end
context UP_cring begin
lemma evalRR_add:
assumes "p \ carrier P" "q \ carrier P"
assumes x: "x \ carrier R"
shows "eval R R id x (p \\<^bsub>P\<^esub> q) = eval R R id x p \ eval R R id x q"
proof -
interpret UP_pre_univ_prop R R id by unfold_locales simp
interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
show ?thesis using assms by simp
qed
lemma evalRR_sub:
assumes "p \ carrier P" "q \ carrier P"
assumes x: "x \ carrier R"
shows "eval R R id x (p \\<^bsub>P\<^esub> q) = eval R R id x p \ eval R R id x q"
proof -
interpret UP_pre_univ_prop R R id by unfold_locales simp
interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
show ?thesis using assms by simp
qed
lemma evalRR_mult:
assumes "p \ carrier P" "q \ carrier P"
assumes x: "x \ carrier R"
shows "eval R R id x (p \\<^bsub>P\<^esub> q) = eval R R id x p \ eval R R id x q"
proof -
interpret UP_pre_univ_prop R R id by unfold_locales simp
interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
show ?thesis using assms by simp
qed
lemma evalRR_monom:
assumes a: "a \ carrier R" and x: "x \ carrier R"
shows "eval R R id x (monom P a d) = a \ x [^] d"
proof -
interpret UP_pre_univ_prop R R id by unfold_locales simp
show ?thesis using assms by (simp add: eval_monom)
qed
lemma evalRR_one:
assumes x: "x \ carrier R"
shows "eval R R id x \\<^bsub>P\<^esub> = \"
proof -
interpret UP_pre_univ_prop R R id by unfold_locales simp
interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
show ?thesis using assms by simp
qed
lemma carrier_evalRR:
assumes x: "x \ carrier R" and "p \ carrier P"
shows "eval R R id x p \ carrier R"
proof -
interpret UP_pre_univ_prop R R id by unfold_locales simp
interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
show ?thesis using assms by simp
qed
lemmas evalRR_simps = evalRR_add evalRR_sub evalRR_mult evalRR_monom evalRR_one carrier_evalRR
end
section \<open>Properties of the Euler \<open>\<phi>\<close>-function\<close>
text_raw \<open>\label{sec:euler-phi}\<close>
text\<open>
In this section we prove that for every positive natural number the equation
$\sum_{d | n}^n \varphi(d) = n$ holds.
\<close>
lemma dvd_div_ge_1:
fixes a b :: nat
assumes "a \ 1" "b dvd a"
shows "a div b \ 1"
proof -
from \<open>b dvd a\<close> obtain c where "a = b * c" ..
with \<open>a \<ge> 1\<close> show ?thesis by simp
qed
lemma dvd_nat_bounds:
fixes n p :: nat
assumes "p > 0" "n dvd p"
shows "n > 0 \ n \ p"
using assms by (simp add: dvd_pos_nat dvd_imp_le)
(* TODO FIXME: This is the "totient" function from HOL-Number_Theory, but since part of
HOL-Number_Theory depends on HOL-Algebra.Multiplicative_Group, there would be a cyclic
dependency. *)
definition phi' :: "nat => nat"
where "phi' m = card {x. 1 \ x \ x \ m \ coprime x m}"
notation (latex output)
phi' ("\ _")
lemma phi'_nonzero:
assumes "m > 0"
shows "phi' m > 0"
proof -
have "1 \ {x. 1 \ x \ x \ m \ coprime x m}" using assms by simp
hence "card {x. 1 \ x \ x \ m \ coprime x m} > 0" by (auto simp: card_gt_0_iff)
thus ?thesis unfolding phi'_def by simp
qed
lemma dvd_div_eq_1:
fixes a b c :: nat
assumes "c dvd a" "c dvd b" "a div c = b div c"
shows "a = b" using assms dvd_mult_div_cancel[OF \<open>c dvd a\<close>] dvd_mult_div_cancel[OF \<open>c dvd b\<close>]
by presburger
lemma dvd_div_eq_2:
fixes a b c :: nat
assumes "c>0" "a dvd c" "b dvd c" "c div a = c div b"
shows "a = b"
proof -
have "a > 0" "a \ c" using dvd_nat_bounds[OF assms(1-2)] by auto
have "a*(c div a) = c" using assms dvd_mult_div_cancel by fastforce
also have "\ = b*(c div a)" using assms dvd_mult_div_cancel by fastforce
finally show "a = b" using \<open>c>0\<close> dvd_div_ge_1[OF _ \<open>a dvd c\<close>] by fastforce
qed
lemma div_mult_mono:
fixes a b c :: nat
assumes "a > 0" "a\d"
shows "a * b div d \ b"
proof -
have "a*b div d \ b*a div a" using assms div_le_mono2 mult.commute[of a b] by presburger
thus ?thesis using assms by force
qed
text\<open>
We arrive at the main result of this section:
For every positive natural number the equation $\sum_{d | n}^n \varphi(d) = n$ holds.
The outline of the proof for this lemma is as follows:
We count the $n$ fractions $1/n$, $\ldots$, $(n-1)/n$, $n/n$.
We analyze the reduced form $a/d = m/n$ for any of those fractions.
We want to know how many fractions $m/n$ have the reduced form denominator $d$.
The condition $1 \leq m \leq n$ is equivalent to the condition $1 \leq a \leq d$.
Therefore we want to know how many $a$ with $1 \leq a \leq d$ exist, s.t. \<^term>\<open>gcd a d = 1\<close>.
This number is exactly \<^term>\<open>phi' d\<close>.
Finally, by counting the fractions $m/n$ according to their reduced form denominator,
we get: @{term [display] "(\d | d dvd n . phi' d) = n"}.
To formalize this proof in Isabelle, we analyze for an arbitrary divisor $d$ of $n$
\begin{itemize}
\item the set of reduced form numerators \<^term>\<open>{a. (1::nat) \<le> a \<and> a \<le> d \<and> coprime a d}\<close>
\item the set of numerators $m$, for which $m/n$ has the reduced form denominator $d$,
i.e. the set \<^term>\<open>{m \<in> {1::nat .. n}. n div gcd m n = d}\<close>
\end{itemize}
We show that \<^term>\<open>\<lambda>a. a*n div d\<close> with the inverse \<^term>\<open>\<lambda>a. a div gcd a n\<close> is
a bijection between theses sets, thus yielding the equality
@{term [display] "phi' d = card {m \ {1 .. n}. n div gcd m n = d}"}
This gives us
@{term [display] "(\d | d dvd n . phi' d)
= card (\<Union>d \<in> {d. d dvd n}. {m \<in> {1 .. n}. n div gcd m n = d})"}
and by showing
\<^term>\<open>(\<Union>d \<in> {d. d dvd n}. {m \<in> {1::nat .. n}. n div gcd m n = d}) \<supseteq> {1 .. n}\<close>
(this is our counting argument) the thesis follows.
\<close>
lemma sum_phi'_factors:
fixes n :: nat
assumes "n > 0"
shows "(\d | d dvd n. phi' d) = n"
proof -
{ fix d assume "d dvd n" then obtain q where q: "n = d * q" ..
have "card {a. 1 \ a \ a \ d \ coprime a d} = card {m \ {1 .. n}. n div gcd m n = d}"
(is "card ?RF = card ?F")
proof (rule card_bij_eq)
{ fix a b assume "a * n div d = b * n div d"
hence "a * (n div d) = b * (n div d)"
using dvd_div_mult[OF \<open>d dvd n\<close>] by (fastforce simp add: mult.commute)
hence "a = b" using dvd_div_ge_1[OF _ \<open>d dvd n\<close>] \<open>n>0\<close>
by (simp add: mult.commute nat_mult_eq_cancel1)
} thus "inj_on (\a. a*n div d) ?RF" unfolding inj_on_def by blast
{ fix a assume a: "a\?RF"
hence "a * (n div d) \ 1" using \n>0\ dvd_div_ge_1[OF _ \d dvd n\] by simp
hence ge_1: "a * n div d \ 1" by (simp add: \d dvd n\ div_mult_swap)
have le_n: "a * n div d \ n" using div_mult_mono a by simp
have "gcd (a * n div d) n = n div d * gcd a d"
by (simp add: gcd_mult_distrib_nat q ac_simps)
hence "n div gcd (a * n div d) n = d*n div (d*(n div d))" using a by simp
hence "a * n div d \ ?F"
using ge_1 le_n by (fastforce simp add: \<open>d dvd n\<close>)
} thus "(\a. a*n div d) ` ?RF \ ?F" by blast
{ fix m l assume A: "m \ ?F" "l \ ?F" "m div gcd m n = l div gcd l n"
hence "gcd m n = gcd l n" using dvd_div_eq_2[OF assms] by fastforce
hence "m = l" using dvd_div_eq_1[of "gcd m n" m l] A(3) by fastforce
} thus "inj_on (\a. a div gcd a n) ?F" unfolding inj_on_def by blast
{ fix m assume "m \ ?F"
hence "m div gcd m n \ ?RF" using dvd_div_ge_1
by (fastforce simp add: div_le_mono div_gcd_coprime)
} thus "(\a. a div gcd a n) ` ?F \ ?RF" by blast
qed force+
} hence phi'_eq: "\d. d dvd n \ phi' d = card {m \ {1 .. n}. n div gcd m n = d}"
unfolding phi'_def by presburger
have fin: "finite {d. d dvd n}" using dvd_nat_bounds[OF \<open>n>0\<close>] by force
have "(\d | d dvd n. phi' d)
= card (\<Union>d \<in> {d. d dvd n}. {m \<in> {1 .. n}. n div gcd m n = d})"
using card_UN_disjoint[OF fin, of "(\d. {m \ {1 .. n}. n div gcd m n = d})"] phi'_eq
by fastforce
also have "(\d \ {d. d dvd n}. {m \ {1 .. n}. n div gcd m n = d}) = {1 .. n}" (is "?L = ?R")
proof
show "?L \ ?R"
proof
fix m assume m: "m \ ?R"
thus "m \ ?L" using dvd_triv_right[of "n div gcd m n" "gcd m n"]
by simp
qed
qed fastforce
finally show ?thesis by force
qed
section \<open>Order of an Element of a Group\<close>
text_raw \<open>\label{sec:order-elem}\<close>
context group begin
definition (in group) ord :: "'a \ nat" where
"ord x \ (@d. \n::nat. x [^] n = \ \ d dvd n)"
lemma (in group) pow_eq_id:
assumes "x \ carrier G"
shows "x [^] n = \ \ (ord x) dvd n"
proof (cases "\n::nat. pow G x n = one G \ n = 0")
case True
show ?thesis
unfolding ord_def
by (rule someI2 [where a=0]) (auto simp: True)
next
case False
define N where "N \ LEAST n::nat. x [^] n = \ \ n > 0"
have N: "x [^] N = \ \ N > 0"
using False
apply (simp add: N_def)
by (metis (mono_tags, lifting) LeastI)
have eq0: "n = 0" if "x [^] n = \" "n < N" for n
using N_def not_less_Least that by fastforce
show ?thesis
unfolding ord_def
proof (rule someI2 [where a = N], rule allI)
fix n :: "nat"
show "(x [^] n = \) \ (N dvd n)"
proof (cases "n = 0")
case False
show ?thesis
unfolding dvd_def
proof safe
assume 1: "x [^] n = \"
have "x [^] n = x [^] (n mod N + N * (n div N))"
by simp
also have "\ = x [^] (n mod N) \ x [^] (N * (n div N))"
by (simp add: assms nat_pow_mult)
also have "\ = x [^] (n mod N)"
by (metis N assms l_cancel_one nat_pow_closed nat_pow_one nat_pow_pow)
finally have "x [^] (n mod N) = \"
by (simp add: "1")
then have "n mod N = 0"
using N eq0 mod_less_divisor by blast
then show "\k. n = N * k"
by blast
next
fix k :: "nat"
assume "n = N * k"
with N show "x [^] (N * k) = \"
by (metis assms nat_pow_one nat_pow_pow)
qed
qed simp
qed blast
qed
lemma (in group) pow_ord_eq_1 [simp]:
"x \ carrier G \ x [^] ord x = \"
by (simp add: pow_eq_id)
lemma (in group) int_pow_eq_id:
assumes "x \ carrier G"
shows "(pow G x i = one G \ int (ord x) dvd i)"
proof (cases i rule: int_cases2)
case (nonneg n)
then show ?thesis
by (simp add: int_pow_int pow_eq_id assms)
next
case (nonpos n)
then have "x [^] i = inv (x [^] n)"
by (simp add: assms int_pow_int int_pow_neg)
then show ?thesis
by (simp add: assms pow_eq_id nonpos)
qed
lemma (in group) int_pow_eq:
"x \ carrier G \ (x [^] m = x [^] n) \ int (ord x) dvd (n - m)"
apply (simp flip: int_pow_eq_id)
by (metis int_pow_closed int_pow_diff inv_closed r_inv right_cancel)
lemma (in group) ord_eq_0:
"x \ carrier G \ (ord x = 0 \ (\n::nat. n \ 0 \ x [^] n \ \))"
by (auto simp: pow_eq_id)
lemma (in group) ord_unique:
"x \ carrier G \ ord x = d \ (\n. pow G x n = one G \ d dvd n)"
by (meson dvd_antisym dvd_refl pow_eq_id)
lemma (in group) ord_eq_1:
"x \ carrier G \ (ord x = 1 \ x = \)"
by (metis pow_eq_id nat_dvd_1_iff_1 nat_pow_eone)
lemma (in group) ord_id [simp]:
"ord (one G) = 1"
using ord_eq_1 by blast
lemma (in group) ord_inv [simp]:
"x \ carrier G
\<Longrightarrow> ord (m_inv G x) = ord x"
by (simp add: ord_unique pow_eq_id nat_pow_inv)
lemma (in group) ord_pow:
assumes "x \ carrier G" "k dvd ord x" "k \ 0"
shows "ord (pow G x k) = ord x div k"
proof -
have "(x [^] k) [^] (ord x div k) = \"
using assms by (simp add: nat_pow_pow)
moreover have "ord x dvd k * ord (x [^] k)"
by (metis assms(1) pow_ord_eq_1 pow_eq_id nat_pow_closed nat_pow_pow)
ultimately show ?thesis
by (metis assms div_dvd_div dvd_antisym dvd_triv_left pow_eq_id nat_pow_closed nonzero_mult_div_cancel_left)
qed
lemma (in group) ord_mul_divides:
assumes eq: "x \ y = y \ x" and xy: "x \ carrier G" "y \ carrier G"
shows "ord (x \ y) dvd (ord x * ord y)"
apply (simp add: xy flip: pow_eq_id eq)
by (metis dvd_triv_left dvd_triv_right eq pow_eq_id one_closed pow_mult_distrib r_one xy)
lemma (in comm_group) abelian_ord_mul_divides:
"\x \ carrier G; y \ carrier G\
\<Longrightarrow> ord (x \<otimes> y) dvd (ord x * ord y)"
by (simp add: ord_mul_divides m_comm)
lemma ord_inj:
assumes a: "a \ carrier G"
shows "inj_on (\ x . a [^] x) {0 .. ord a - 1}"
proof -
let ?M = "Max (ord ` carrier G)"
have "finite {d \ {..?M}. a [^] d = \}" by auto
have *: False if A: "x < y" "x \ {0 .. ord a - 1}" "y \ {0 .. ord a - 1}"
"a [^] x = a [^] y" for x y
proof -
have "y - x < ord a" using that by auto
moreover have "a [^] (y-x) = \" using a A by (simp add: pow_eq_div2)
ultimately have "min (y - x) (ord a) = ord a"
using A(1) a pow_eq_id by auto
with \<open>y - x < ord a\<close> show False by linarith
qed
show ?thesis
unfolding inj_on_def by (metis nat_neq_iff *)
qed
lemma ord_inj':
assumes a: "a \ carrier G"
shows "inj_on (\ x . a [^] x) {1 .. ord a}"
proof (rule inj_onI, rule ccontr)
fix x y :: nat
assume A: "x \ {1 .. ord a}" "y \ {1 .. ord a}" "a [^] x = a [^] y" "x\y"
{ assume "x < ord a" "y < ord a"
hence False using ord_inj[OF assms] A unfolding inj_on_def by fastforce
}
moreover
{ assume "x = ord a" "y < ord a"
hence "a [^] y = a [^] (0::nat)" using pow_ord_eq_1 A by (simp add: a)
hence "y=0" using ord_inj[OF assms] \<open>y < ord a\<close> unfolding inj_on_def by force
hence False using A by fastforce
}
moreover
{ assume "y = ord a" "x < ord a"
hence "a [^] x = a [^] (0::nat)" using pow_ord_eq_1 A by (simp add: a)
hence "x=0" using ord_inj[OF assms] \<open>x < ord a\<close> unfolding inj_on_def by force
hence False using A by fastforce
}
ultimately show False using A by force
qed
lemma (in group) ord_ge_1:
assumes finite: "finite (carrier G)" and a: "a \ carrier G"
shows "ord a \ 1"
proof -
have "((\n::nat. a [^] n) ` {0<..}) \ carrier G"
using a by blast
then have "finite ((\n::nat. a [^] n) ` {0<..})"
using finite_subset finite by auto
then have "\ inj_on (\n::nat. a [^] n) {0<..}"
using finite_imageD infinite_Ioi by blast
then obtain i j::nat where "i \ j" "a [^] i = a [^] j"
by (auto simp: inj_on_def)
then have "\n::nat. n>0 \ a [^] n = \"
by (metis a diffs0_imp_equal pow_eq_div2 neq0_conv)
then have "ord a \ 0"
by (simp add: ord_eq_0 [OF a])
then show ?thesis
by simp
qed
lemma ord_elems:
assumes "finite (carrier G)" "a \ carrier G"
shows "{a[^]x | x. x \ (UNIV :: nat set)} = {a[^]x | x. x \ {0 .. ord a - 1}}" (is "?L = ?R")
proof
show "?R \ ?L" by blast
{ fix y assume "y \ ?L"
then obtain x::nat where x: "y = a[^]x" by auto
define r q where "r = x mod ord a" and "q = x div ord a"
then have "x = q * ord a + r"
by (simp add: div_mult_mod_eq)
hence "y = (a[^]ord a)[^]q \ a[^]r"
using x assms by (metis mult.commute nat_pow_mult nat_pow_pow)
hence "y = a[^]r" using assms by (simp add: pow_ord_eq_1)
have "r < ord a" using ord_ge_1[OF assms] by (simp add: r_def)
hence "r \ {0 .. ord a - 1}" by (force simp: r_def)
hence "y \ {a[^]x | x. x \ {0 .. ord a - 1}}" using \y=a[^]r\ by blast
}
thus "?L \ ?R" by auto
qed
lemma (in group)
assumes "x \ carrier G"
shows finite_cyclic_subgroup:
"finite(carrier(subgroup_generated G {x})) \ (\n::nat. n \ 0 \ x [^] n = \)" (is "?fin \ ?nat1")
and infinite_cyclic_subgroup:
"infinite(carrier(subgroup_generated G {x})) \ (\m n::nat. x [^] m = x [^] n \ m = n)" (is "\ ?fin \ ?nateq")
and finite_cyclic_subgroup_int:
"finite(carrier(subgroup_generated G {x})) \ (\i::int. i \ 0 \ x [^] i = \)" (is "?fin \ ?int1")
and infinite_cyclic_subgroup_int:
"infinite(carrier(subgroup_generated G {x})) \ (\i j::int. x [^] i = x [^] j \ i = j)" (is "\ ?fin \ ?inteq")
proof -
have 1: "\ ?fin" if ?nateq
proof -
have "infinite (range (\n::nat. x [^] n))"
using that range_inj_infinite [of "(\n::nat. x [^] n)"] by (auto simp: inj_on_def)
moreover have "range (\n::nat. x [^] n) \ range (\i::int. x [^] i)"
apply clarify
by (metis assms group.int_pow_neg int_pow_closed int_pow_neg_int is_group local.inv_equality nat_pow_closed r_inv rangeI)
ultimately show ?thesis
using carrier_subgroup_generated_by_singleton [OF assms] finite_subset by auto
qed
have 2: "m = n" if mn: "x [^] m = x [^] n" and eq [rule_format]: "?inteq" for m n::nat
using eq [of "int m" "int n"]
by (simp add: int_pow_int mn)
have 3: ?nat1 if non: "\ ?inteq"
proof -
obtain i j::int where eq: "x [^] i = x [^] j" and "i \ j"
using non by auto
show ?thesis
proof (cases i j rule: linorder_cases)
case less
then have [simp]: "x [^] (j - i) = \"
by (simp add: eq assms int_pow_diff)
show ?thesis
using less by (rule_tac x="nat (j-i)" in exI) auto
next
case greater
then have [simp]: "x [^] (i - j) = \"
by (simp add: eq assms int_pow_diff)
then show ?thesis
using greater by (rule_tac x="nat (i-j)" in exI) auto
qed (use \<open>i \<noteq> j\<close> in auto)
qed
have 4: "\i::int. (i \ 0) \ x [^] i = \" if "n \ 0" "x [^] n = \" for n::nat
apply (rule_tac x="int n" in exI)
by (simp add: int_pow_int that)
have 5: "finite (carrier (subgroup_generated G {x}))" if "i \ 0" and 1: "x [^] i = \" for i::int
proof -
obtain n::nat where n: "n > 0" "x [^] n = \"
using "1" "3" \<open>i \<noteq> 0\<close> by fastforce
have "x [^] a \ ([^]) x ` {0..
proof
show "x [^] a = x [^] nat (a mod int n)"
using n
by simp (metis (no_types, lifting) assms dvd_minus_mod dvd_trans int_pow_eq int_pow_eq_id int_pow_int)
show "nat (a mod int n) \ {0..
using n apply (simp add: split: split_nat)
using Euclidean_Division.pos_mod_bound by presburger
qed
then have "carrier (subgroup_generated G {x}) \ ([^]) x ` {0..
using carrier_subgroup_generated_by_singleton [OF assms] by auto
then show ?thesis
using finite_surj by blast
qed
show "?fin \ ?nat1" "\ ?fin \ ?nateq" "?fin \ ?int1" "\ ?fin \ ?inteq"
using 1 2 3 4 5 by meson+
qed
lemma (in group) finite_cyclic_subgroup_order:
"x \ carrier G \ finite(carrier(subgroup_generated G {x})) \ ord x \ 0"
by (simp add: finite_cyclic_subgroup ord_eq_0)
lemma (in group) infinite_cyclic_subgroup_order:
"x \ carrier G \ infinite (carrier(subgroup_generated G {x})) \ ord x = 0"
by (simp add: finite_cyclic_subgroup_order)
lemma generate_pow_on_finite_carrier: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
assumes "finite (carrier G)" and a: "a \ carrier G"
shows "generate G { a } = { a [^] k | k. k \ (UNIV :: nat set) }"
proof
show "{ a [^] k | k. k \ (UNIV :: nat set) } \ generate G { a }"
proof
fix b assume "b \ { a [^] k | k. k \ (UNIV :: nat set) }"
then obtain k :: nat where "b = a [^] k" by blast
hence "b = a [^] (int k)"
by (simp add: int_pow_int)
thus "b \ generate G { a }"
unfolding generate_pow[OF a] by blast
qed
next
show "generate G { a } \ { a [^] k | k. k \ (UNIV :: nat set) }"
proof
fix b assume "b \ generate G { a }"
then obtain k :: int where k: "b = a [^] k"
unfolding generate_pow[OF a] by blast
show "b \ { a [^] k | k. k \ (UNIV :: nat set) }"
proof (cases "k < 0")
assume "\ k < 0"
hence "b = a [^] (nat k)"
by (simp add: k)
thus ?thesis by blast
next
assume "k < 0"
hence b: "b = inv (a [^] (nat (- k)))"
using k a by (auto simp: int_pow_neg)
obtain m where m: "ord a * m \ nat (- k)"
by (metis assms mult.left_neutral mult_le_mono1 ord_ge_1)
hence "a [^] (ord a * m) = \"
by (metis a nat_pow_one nat_pow_pow pow_ord_eq_1)
then obtain k' :: nat where "(a [^] (nat (- k))) \ (a [^] k') = \"
using m a nat_le_iff_add nat_pow_mult by auto
hence "b = a [^] k'"
using b a by (metis inv_unique' nat_pow_closed nat_pow_comm)
thus "b \ { a [^] k | k. k \ (UNIV :: nat set) }" by blast
qed
qed
qed
lemma ord_elems_inf_carrier:
assumes "a \ carrier G" "ord a \ 0"
shows "{a[^]x | x. x \ (UNIV :: nat set)} = {a[^]x | x. x \ {0 .. ord a - 1}}" (is "?L = ?R")
proof
show "?R \ ?L" by blast
{ fix y assume "y \ ?L"
then obtain x::nat where x: "y = a[^]x" by auto
define r q where "r = x mod ord a" and "q = x div ord a"
then have "x = q * ord a + r"
by (simp add: div_mult_mod_eq)
hence "y = (a[^]ord a)[^]q \ a[^]r"
using x assms by (metis mult.commute nat_pow_mult nat_pow_pow)
hence "y = a[^]r" using assms by simp
have "r < ord a" using assms by (simp add: r_def)
hence "r \ {0 .. ord a - 1}" by (force simp: r_def)
hence "y \ {a[^]x | x. x \ {0 .. ord a - 1}}" using \y=a[^]r\ by blast
}
thus "?L \ ?R" by auto
qed
lemma generate_pow_nat:
assumes a: "a \ carrier G" and "ord a \ 0"
shows "generate G { a } = { a [^] k | k. k \ (UNIV :: nat set) }"
proof
show "{ a [^] k | k. k \ (UNIV :: nat set) } \ generate G { a }"
proof
fix b assume "b \ { a [^] k | k. k \ (UNIV :: nat set) }"
then obtain k :: nat where "b = a [^] k" by blast
hence "b = a [^] (int k)"
by (simp add: int_pow_int)
thus "b \ generate G { a }"
unfolding generate_pow[OF a] by blast
qed
next
show "generate G { a } \ { a [^] k | k. k \ (UNIV :: nat set) }"
proof
fix b assume "b \ generate G { a }"
then obtain k :: int where k: "b = a [^] k"
unfolding generate_pow[OF a] by blast
show "b \ { a [^] k | k. k \ (UNIV :: nat set) }"
proof (cases "k < 0")
assume "\ k < 0"
hence "b = a [^] (nat k)"
by (simp add: k)
thus ?thesis by blast
next
assume "k < 0"
hence b: "b = inv (a [^] (nat (- k)))"
using k a by (auto simp: int_pow_neg)
obtain m where m: "ord a * m \ nat (- k)"
by (metis assms(2) dvd_imp_le dvd_triv_right le_zero_eq mult_eq_0_iff not_gr_zero)
hence "a [^] (ord a * m) = \"
by (metis a nat_pow_one nat_pow_pow pow_ord_eq_1)
then obtain k' :: nat where "(a [^] (nat (- k))) \ (a [^] k') = \"
using m a nat_le_iff_add nat_pow_mult by auto
hence "b = a [^] k'"
using b a by (metis inv_unique' nat_pow_closed nat_pow_comm)
thus "b \ { a [^] k | k. k \ (UNIV :: nat set) }" by blast
qed
qed
qed
lemma generate_pow_card:
assumes a: "a \ carrier G"
shows "ord a = card (generate G { a })"
proof (cases "ord a = 0")
case True
then have "infinite (carrier (subgroup_generated G {a}))"
using infinite_cyclic_subgroup_order[OF a] by auto
then have "infinite (generate G {a})"
unfolding subgroup_generated_def
using a by simp
then show ?thesis
using \<open>ord a = 0\<close> by auto
next
case False
note finite_subgroup = this
then have "generate G { a } = (([^]) a) ` {0..ord a - 1}"
using generate_pow_nat ord_elems_inf_carrier a by auto
hence "card (generate G {a}) = card {0..ord a - 1}"
using ord_inj[OF a] card_image by metis
also have "... = ord a" using finite_subgroup by auto
finally show ?thesis..
qed
lemma (in group) cyclic_order_is_ord:
assumes "g \ carrier G"
shows "ord g = order (subgroup_generated G {g})"
unfolding order_def subgroup_generated_def
using assms generate_pow_card by simp
lemma ord_dvd_group_order:
assumes "a \ carrier G" shows "(ord a) dvd (order G)"
using lagrange[OF generate_is_subgroup[of "{a}"]] assms
unfolding generate_pow_card[OF assms]
by (metis dvd_triv_right empty_subsetI insert_subset)
lemma (in group) pow_order_eq_1:
assumes "a \ carrier G" shows "a [^] order G = \"
using assms by (metis nat_pow_pow ord_dvd_group_order pow_ord_eq_1 dvdE nat_pow_one)
lemma dvd_gcd:
fixes a b :: nat
obtains q where "a * (b div gcd a b) = b*q"
proof
have "a * (b div gcd a b) = (a div gcd a b) * b" by (simp add: div_mult_swap dvd_div_mult)
also have "\ = b * (a div gcd a b)" by simp
finally show "a * (b div gcd a b) = b * (a div gcd a b) " .
qed
lemma (in group) ord_le_group_order:
assumes finite: "finite (carrier G)" and a: "a \ carrier G"
shows "ord a \ order G"
by (simp add: a dvd_imp_le local.finite ord_dvd_group_order order_gt_0_iff_finite)
lemma (in group) ord_pow_gen:
assumes "x \ carrier G"
shows "ord (pow G x k) = (if k = 0 then 1 else ord x div gcd (ord x) k)"
proof -
have "ord (x [^] k) = ord x div gcd (ord x) k"
if "0 < k"
proof -
have "(d dvd k * n) = (d div gcd (d) k dvd n)" for d n
using that by (simp add: div_dvd_iff_mult gcd_mult_distrib_nat mult.commute)
then show ?thesis
using that by (auto simp add: assms ord_unique nat_pow_pow pow_eq_id)
qed
then show ?thesis by auto
qed
lemma (in group)
assumes finite': "finite (carrier G)" "a \ carrier G"
shows pow_ord_eq_ord_iff: "group.ord G (a [^] k) = ord a \ coprime k (ord a)" (is "?L \ ?R")
using assms ord_ge_1 [OF assms]
by (auto simp: div_eq_dividend_iff ord_pow_gen coprime_iff_gcd_eq_1 gcd.commute split: if_split_asm)
lemma element_generates_subgroup:
assumes finite[simp]: "finite (carrier G)"
assumes a[simp]: "a \ carrier G"
shows "subgroup {a [^] i | i. i \ {0 .. ord a - 1}} G"
using generate_is_subgroup[of "{ a }"] assms(2)
generate_pow_on_finite_carrier[OF assms]
unfolding ord_elems[OF assms] by auto
end
section \<open>Number of Roots of a Polynomial\<close>
text_raw \<open>\label{sec:number-roots}\<close>
definition mult_of :: "('a, 'b) ring_scheme \ 'a monoid" where
"mult_of R \ \ carrier = carrier R - {\\<^bsub>R\<^esub>}, mult = mult R, one = \\<^bsub>R\<^esub>\"
lemma carrier_mult_of [simp]: "carrier (mult_of R) = carrier R - {\\<^bsub>R\<^esub>}"
by (simp add: mult_of_def)
lemma mult_mult_of [simp]: "mult (mult_of R) = mult R"
by (simp add: mult_of_def)
lemma nat_pow_mult_of: "([^]\<^bsub>mult_of R\<^esub>) = (([^]\<^bsub>R\<^esub>) :: _ \ nat \ _)"
by (simp add: mult_of_def fun_eq_iff nat_pow_def)
lemma one_mult_of [simp]: "\\<^bsub>mult_of R\<^esub> = \\<^bsub>R\<^esub>"
by (simp add: mult_of_def)
lemmas mult_of_simps = carrier_mult_of mult_mult_of nat_pow_mult_of one_mult_of
context field
begin
lemma mult_of_is_Units: "mult_of R = units_of R"
unfolding mult_of_def units_of_def using field_Units by auto
lemma m_inv_mult_of:
"\x. x \ carrier (mult_of R) \ m_inv (mult_of R) x = m_inv R x"
using mult_of_is_Units units_of_inv unfolding units_of_def
by simp
lemma (in field) field_mult_group: "group (mult_of R)"
proof (rule groupI)
show "\y\carrier (mult_of R). y \\<^bsub>mult_of R\<^esub> x = \\<^bsub>mult_of R\<^esub>"
if "x \ carrier (mult_of R)" for x
using group.l_inv_ex mult_of_is_Units that units_group by fastforce
qed (auto simp: m_assoc dest: integral)
lemma finite_mult_of: "finite (carrier R) \ finite (carrier (mult_of R))"
by simp
lemma order_mult_of: "finite (carrier R) \ order (mult_of R) = order R - 1"
unfolding order_def carrier_mult_of by (simp add: card.remove)
end
lemma (in monoid) Units_pow_closed :
fixes d :: nat
assumes "x \ Units G"
shows "x [^] d \ Units G"
by (metis assms group.is_monoid monoid.nat_pow_closed units_group units_of_carrier units_of_pow)
lemma (in ring) r_right_minus_eq[simp]:
assumes "a \ carrier R" "b \ carrier R"
shows "a \ b = \ \ a = b"
using assms by (metis a_minus_def add.inv_closed minus_equality r_neg)
context UP_cring begin
lemma is_UP_cring: "UP_cring R" by (unfold_locales)
lemma is_UP_ring:
shows "UP_ring R" by (unfold_locales)
end
context UP_domain begin
lemma roots_bound:
assumes f [simp]: "f \ carrier P"
assumes f_not_zero: "f \ \\<^bsub>P\<^esub>"
assumes finite: "finite (carrier R)"
shows "finite {a \ carrier R . eval R R id a f = \} \
card {a \<in> carrier R . eval R R id a f = \<zero>} \<le> deg R f" using f f_not_zero
proof (induction "deg R f" arbitrary: f)
case 0
have "\x. eval R R id x f \ \"
proof -
fix x
have "(\i\{..deg R f}. id (coeff P f i) \ x [^] i) \ \"
using 0 lcoeff_nonzero_nonzero[where p = f] by simp
thus "eval R R id x f \ \" using 0 unfolding eval_def P_def by simp
qed
then have *: "{a \ carrier R. eval R R (\a. a) a f = \} = {}"
by (auto simp: id_def)
show ?case by (simp add: *)
next
case (Suc x)
show ?case
proof (cases "\ a \ carrier R . eval R R id a f = \")
case True
then obtain a where a_carrier[simp]: "a \ carrier R" and a_root: "eval R R id a f = \" by blast
have R_not_triv: "carrier R \ {\}"
by (metis R.one_zeroI R.zero_not_one)
obtain q where q: "(q \ carrier P)" and
f: "f = (monom P \\<^bsub>R\<^esub> 1 \\<^bsub> P\<^esub> monom P a 0) \\<^bsub>P\<^esub> q \\<^bsub>P\<^esub> monom P (eval R R id a f) 0"
using remainder_theorem[OF Suc.prems(1) a_carrier R_not_triv] by auto
hence lin_fac: "f = (monom P \\<^bsub>R\<^esub> 1 \\<^bsub> P\<^esub> monom P a 0) \\<^bsub>P\<^esub> q" using q by (simp add: a_root)
have deg: "deg R (monom P \\<^bsub>R\<^esub> 1 \\<^bsub> P\<^esub> monom P a 0) = 1"
using a_carrier by (simp add: deg_minus_eq)
hence mon_not_zero: "(monom P \\<^bsub>R\<^esub> 1 \\<^bsub> P\<^esub> monom P a 0) \ \\<^bsub>P\<^esub>"
by (fastforce simp del: r_right_minus_eq)
have q_not_zero: "q \ \\<^bsub>P\<^esub>" using Suc by (auto simp add : lin_fac)
hence "deg R q = x" using Suc deg deg_mult[OF mon_not_zero q_not_zero _ q]
by (simp add : lin_fac)
hence q_IH: "finite {a \ carrier R . eval R R id a q = \}
\<and> card {a \<in> carrier R . eval R R id a q = \<zero>} \<le> x" using Suc q q_not_zero by blast
have subs: "{a \ carrier R . eval R R id a f = \}
\<subseteq> {a \<in> carrier R . eval R R id a q = \<zero>} \<union> {a}" (is "?L \<subseteq> ?R \<union> {a}")
using a_carrier \<open>q \<in> _\<close>
by (auto simp: evalRR_simps lin_fac R.integral_iff)
have "{a \ carrier R . eval R R id a f = \} \ insert a {a \ carrier R . eval R R id a q = \}"
using subs by auto
hence "card {a \ carrier R . eval R R id a f = \} \
card (insert a {a \<in> carrier R . eval R R id a q = \<zero>})" using q_IH by (blast intro: card_mono)
also have "\ \ deg R f" using q_IH \Suc x = _\
by (simp add: card_insert_if)
finally show ?thesis using q_IH \<open>Suc x = _\<close> using finite by force
next
case False
hence "card {a \ carrier R. eval R R id a f = \} = 0" using finite by auto
also have "\ \ deg R f" by simp
finally show ?thesis using finite by auto
qed
qed
end
lemma (in domain) num_roots_le_deg :
fixes p d :: nat
assumes finite: "finite (carrier R)"
assumes d_neq_zero: "d \ 0"
shows "card {x \ carrier R. x [^] d = \} \ d"
proof -
let ?f = "monom (UP R) \\<^bsub>R\<^esub> d \\<^bsub> (UP R)\<^esub> monom (UP R) \\<^bsub>R\<^esub> 0"
have one_in_carrier: "\ \ carrier R" by simp
interpret R: UP_domain R "UP R" by (unfold_locales)
have "deg R ?f = d"
using d_neq_zero by (simp add: R.deg_minus_eq)
hence f_not_zero: "?f \ \\<^bsub>UP R\<^esub>" using d_neq_zero by (auto simp add : R.deg_nzero_nzero)
have roots_bound: "finite {a \ carrier R . eval R R id a ?f = \} \
card {a \<in> carrier R . eval R R id a ?f = \<zero>} \<le> deg R ?f"
using finite by (intro R.roots_bound[OF _ f_not_zero]) simp
have subs: "{x \ carrier R. x [^] d = \} \ {a \ carrier R . eval R R id a ?f = \}"
by (auto simp: R.evalRR_simps)
then have "card {x \ carrier R. x [^] d = \} \
card {a \<in> carrier R. eval R R id a ?f = \<zero>}" using finite by (simp add : card_mono)
thus ?thesis using \<open>deg R ?f = d\<close> roots_bound by linarith
qed
section \<open>The Multiplicative Group of a Field\<close>
text_raw \<open>\label{sec:mult-group}\<close>
text \<open>
In this section we show that the multiplicative group of a finite field
is generated by a single element, i.e. it is cyclic. The proof is inspired
by the first proof given in the survey~@{cite "conrad-cyclicity"}.
\<close>
context field begin
lemma num_elems_of_ord_eq_phi':
assumes finite: "finite (carrier R)" and dvd: "d dvd order (mult_of R)"
and exists: "\a\carrier (mult_of R). group.ord (mult_of R) a = d"
shows "card {a \ carrier (mult_of R). group.ord (mult_of R) a = d} = phi' d"
proof -
note mult_of_simps[simp]
have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of)
interpret G:group "mult_of R" rewrites "([^]\<^bsub>mult_of R\<^esub>) = (([^]) :: _ \ nat \ _)" and "\\<^bsub>mult_of R\<^esub> = \"
by (rule field_mult_group) simp_all
from exists
obtain a where a: "a \ carrier (mult_of R)" and ord_a: "group.ord (mult_of R) a = d"
by (auto simp add: card_gt_0_iff)
have set_eq1: "{a[^]n| n. n \ {1 .. d}} = {x \ carrier (mult_of R). x [^] d = \}"
proof (rule card_seteq)
show "finite {x \ carrier (mult_of R). x [^] d = \}" using finite by auto
show "{a[^]n| n. n \ {1 ..d}} \ {x \ carrier (mult_of R). x[^]d = \}"
proof
fix x assume "x \ {a[^]n | n. n \ {1 .. d}}"
then obtain n where n: "x = a[^]n \ n \ {1 .. d}" by auto
have "x[^]d =(a[^]d)[^]n" using n a ord_a by (simp add:nat_pow_pow mult.commute)
hence "x[^]d = \" using ord_a G.pow_ord_eq_1[OF a] by fastforce
thus "x \ {x \ carrier (mult_of R). x[^]d = \}" using G.nat_pow_closed[OF a] n by blast
qed
show "card {x \ carrier (mult_of R). x [^] d = \} \ card {a[^]n | n. n \ {1 .. d}}"
proof -
have *: "{a[^]n | n. n \ {1 .. d }} = ((\ n. a[^]n) ` {1 .. d})" by auto
have "0 < order (mult_of R)" unfolding order_mult_of[OF finite]
using card_mono[OF finite, of "{\, \}"] by (simp add: order_def)
have "card {x \ carrier (mult_of R). x [^] d = \} \ card {x \ carrier R. x [^] d = \}"
using finite by (auto intro: card_mono)
also have "\ \ d" using \0 < order (mult_of R)\ num_roots_le_deg[OF finite, of d]
by (simp add : dvd_pos_nat[OF _ \<open>d dvd order (mult_of R)\<close>])
finally show ?thesis using G.ord_inj'[OF a] ord_a * by (simp add: card_image)
qed
qed
have set_eq2: "{x \ carrier (mult_of R) . group.ord (mult_of R) x = d}
= (\<lambda> n . a[^]n) ` {n \<in> {1 .. d}. group.ord (mult_of R) (a[^]n) = d}" (is "?L = ?R")
proof
{ fix x assume x: "x \ (carrier (mult_of R)) \ group.ord (mult_of R) x = d"
hence "x \ {x \ carrier (mult_of R). x [^] d = \}"
by (simp add: G.pow_ord_eq_1[of x, symmetric])
then obtain n where n: "x = a[^]n \ n \ {1 .. d}" using set_eq1 by blast
hence "x \ ?R" using x by fast
} thus "?L \ ?R" by blast
show "?R \ ?L" using a by (auto simp add: carrier_mult_of[symmetric] simp del: carrier_mult_of)
qed
have "inj_on (\ n . a[^]n) {n \ {1 .. d}. group.ord (mult_of R) (a[^]n) = d}"
using G.ord_inj'[OF a, unfolded ord_a] unfolding inj_on_def by fast
hence "card ((\n. a[^]n) ` {n \ {1 .. d}. group.ord (mult_of R) (a[^]n) = d})
= card {k \<in> {1 .. d}. group.ord (mult_of R) (a[^]k) = d}"
using card_image by blast
thus ?thesis using set_eq2 G.pow_ord_eq_ord_iff[OF finite' \a \ _\, unfolded ord_a]
by (simp add: phi'_def)
qed
end
theorem (in field) finite_field_mult_group_has_gen :
assumes finite: "finite (carrier R)"
shows "\ a \ carrier (mult_of R) . carrier (mult_of R) = {a[^]i | i::nat . i \ UNIV}"
proof -
note mult_of_simps[simp]
have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of)
interpret G: group "mult_of R" rewrites
"([^]\<^bsub>mult_of R\<^esub>) = (([^]) :: _ \ nat \ _)" and "\\<^bsub>mult_of R\<^esub> = \"
by (rule field_mult_group) (simp_all add: fun_eq_iff nat_pow_def)
let ?N = "\ x . card {a \ carrier (mult_of R). group.ord (mult_of R) a = x}"
have "0 < order R - 1" unfolding order_def using card_mono[OF finite, of "{\, \}"] by simp
then have *: "0 < order (mult_of R)" using assms by (simp add: order_mult_of)
have fin: "finite {d. d dvd order (mult_of R) }" using dvd_nat_bounds[OF *] by force
have "(\d | d dvd order (mult_of R). ?N d)
= card (UN d:{d . d dvd order (mult_of R) }. {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d})"
(is "_ = card ?U")
using fin finite by (subst card_UN_disjoint) auto
also have "?U = carrier (mult_of R)"
proof
{ fix x assume x: "x \ carrier (mult_of R)"
hence x': "x\carrier (mult_of R)" by simp
then have "group.ord (mult_of R) x dvd order (mult_of R)"
using G.ord_dvd_group_order by blast
hence "x \ ?U" using dvd_nat_bounds[of "order (mult_of R)" "group.ord (mult_of R) x"] x by blast
} thus "carrier (mult_of R) \ ?U" by blast
qed auto
also have "card ... = order (mult_of R)"
using order_mult_of finite' by (simp add: order_def)
finally have sum_Ns_eq: "(\d | d dvd order (mult_of R). ?N d) = order (mult_of R)" .
{ fix d assume d: "d dvd order (mult_of R)"
have "card {a \ carrier (mult_of R). group.ord (mult_of R) a = d} \ phi' d"
proof cases
assume "card {a \ carrier (mult_of R). group.ord (mult_of R) a = d} = 0" thus ?thesis by presburger
next
assume "card {a \ carrier (mult_of R). group.ord (mult_of R) a = d} \ 0"
hence "\a \ carrier (mult_of R). group.ord (mult_of R) a = d" by (auto simp: card_eq_0_iff)
thus ?thesis using num_elems_of_ord_eq_phi'[OF finite d] by auto
qed
}
hence all_le: "\i. i \ {d. d dvd order (mult_of R) }
\<Longrightarrow> (\<lambda>i. card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = i}) i \<le> (\<lambda>i. phi' i) i" by fast
hence le: "(\i | i dvd order (mult_of R). ?N i)
\<le> (\<Sum>i | i dvd order (mult_of R). phi' i)"
using sum_mono[of "{d . d dvd order (mult_of R)}"
"\i. card {a \ carrier (mult_of R). group.ord (mult_of R) a = i}"] by presburger
have "order (mult_of R) = (\d | d dvd order (mult_of R). phi' d)" using *
by (simp add: sum_phi'_factors)
hence eq: "(\i | i dvd order (mult_of R). ?N i)
= (\<Sum>i | i dvd order (mult_of R). phi' i)" using le sum_Ns_eq by presburger
have "\i. i \ {d. d dvd order (mult_of R) } \ ?N i = (\i. phi' i) i"
proof (rule ccontr)
fix i
assume i1: "i \ {d. d dvd order (mult_of R)}" and "?N i \ phi' i"
hence "?N i = 0"
using num_elems_of_ord_eq_phi'[OF finite, of i] by (auto simp: card_eq_0_iff)
moreover have "0 < i" using * i1 by (simp add: dvd_nat_bounds[of "order (mult_of R)" i])
ultimately have "?N i < phi' i" using phi'_nonzero by presburger
hence "(\i | i dvd order (mult_of R). ?N i)
< (\<Sum>i | i dvd order (mult_of R). phi' i)"
using sum_strict_mono_ex1[OF fin, of "?N" "\ i . phi' i"]
i1 all_le by auto
thus False using eq by force
qed
hence "?N (order (mult_of R)) > 0" using * by (simp add: phi'_nonzero)
then obtain a where a: "a \ carrier (mult_of R)" and a_ord: "group.ord (mult_of R) a = order (mult_of R)"
by (auto simp add: card_gt_0_iff)
hence set_eq: "{a[^]i | i::nat. i \ UNIV} = (\x. a[^]x) ` {0 .. group.ord (mult_of R) a - 1}"
using G.ord_elems[OF finite'] by auto
have card_eq: "card ((\x. a[^]x) ` {0 .. group.ord (mult_of R) a - 1}) = card {0 .. group.ord (mult_of R) a - 1}"
by (intro card_image G.ord_inj finite' a)
hence "card ((\ x . a[^]x) ` {0 .. group.ord (mult_of R) a - 1}) = card {0 ..order (mult_of R) - 1}"
using assms by (simp add: card_eq a_ord)
hence card_R_minus_1: "card {a[^]i | i::nat. i \ UNIV} = order (mult_of R)"
using * by (subst set_eq) auto
have **: "{a[^]i | i::nat. i \ UNIV} \ carrier (mult_of R)"
using G.nat_pow_closed[OF a] by auto
with _ have "carrier (mult_of R) = {a[^]i|i::nat. i \ UNIV}"
by (rule card_seteq[symmetric]) (simp_all add: card_R_minus_1 finite order_def del: UNIV_I)
thus ?thesis using a by blast
qed
end
¤ Dauer der Verarbeitung: 0.88 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
|
|
|
|
|
