1

我试图证明欧拉标准的一种非常有限的形式：

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。我在这里错过了什么吗？

顺便说一句，我也可能完全错过了数学计算库本身中已经存在的欧拉准则证明。

4

1 回答 1

2

我不知道欧拉准则的证明，但我在 finfield 中发现了两个引理，它们为您提供了完成证明所需的两个结果（第二个可能不会按您的预期呈现）：

首先，您有以下引理，它为您提供p与您的领域特征相对应的素数F（只要它是 a 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.
于 2018-06-27T09:56:36.477 回答