Мощность 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). Кажется, я не могу найти полезных фактов в библиотеке математических композиций о количестве элементов finFieldTypes. Например, я ожидаю, что лемма о том, что существует p такой, что prime p а также #|F| = p, Я что-то здесь упускаю?

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

Answer 1

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

Во-первых, у вас есть следующая лемма, которая дает вам простое 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 с явной характеристикой. Но, учитывая первую лемму, вы можете создать такую ​​структуру для своего поля (которое имеет канонический тип 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.