Мощность finFieldType / критерий Эйлера

Question

Я пытаюсь доказать очень ограниченную форму критерия Эйлера:

Variable F : finFieldType.
Hypothesis HF : (1 != -1 :> F).
Lemma euler (a : F) : a^+(#|F|.-1./2) = -1 -> forall x, x^+2 != a.

У меня уже есть большая часть доказательства, но у меня осталось odd (#|F|.-1) = 0, то есть #|F|.-1даже.(Меня не интересует характеристика 2).Я не могу найти полезных фактов в библиотеке математических композиций о мощности finFieldType с.Например, я бы ожидал лемму о том, что существует p такое, что prime p и #|F| = p.Я что-то здесь упускаю?

Кстати, я мог бы также полностью пропустить уже существующее доказательство критерия Эйлера в самой библиотеке математических вычислений.

Answer 1

Мне неизвестно о доказательстве критерия Эйлера, но я нашел две леммы в финфилде, которые дают вам два результата, которые вы ожидали, чтобы закончить доказательство (второй может быть представлен не так, как вы ожидали):

Во-первых, у вас есть следующая лемма, которая дает вам простое число p, соответствующее характеристике вашего поля F (при условии, что это finFieldType):

Lemma finCharP : {p | prime p & p \in [char F]}.

Затем другая лемма дает вам аргумент мощности:

Let n := logn p #|R|.
Lemma card_primeChar : #|R| = (p ^ n)%N.

Проблема со второй леммой состоит в том, что ваше поле должно быть распознано как PrimeCharType, что примерно соответствует ringType с явной характеристикой.Но, учитывая первую лемму, вы можете создать такую ​​структуру для своего поля (которое канонически имеет тип кольца) на лету.Возможным доказательством может быть следующее

Lemma odd_card : ~~ odd (#|F|.-1).
Proof.
suff : odd (#|F|) by have /ltnW/prednK {1}<- /= := finRing_gt1 F.
have [p prime_p char_F] := (finCharP F); set F_pC := PrimeCharType p_char.
have H : #|F| = #|F_primeChar| by []; rewrite H card_primeChar -H odd_exp => {H F_pC}.
apply/orP; right; have := HF; apply: contraR=> /(prime_oddPn prime_p) p_eq2.
by move: char_F; rewrite p_eq2=> /oppr_char2 ->.
Qed.