Lemma Derivation_separableP :
-
reflect
- (
∀ D,
Derivation <<K; x>> D → K ≤ lker D → <<K; x>> ≤ lker D)%
VS
+
reflect
+ (
∀ D,
Derivation <<K; x>> D → K ≤ lker D → <<K; x>> ≤ lker D)%
VS
(
separable_element K x).
@@ -308,69 +307,69 @@ http://www.math.uconn.edu/~kconrad/blurbs/galoistheory/separable2.pdf
Lemma separable_elementS K E x :
- (
K ≤ E)%
VS → separable_element K x → separable_element E x.
+ (
K ≤ E)%
VS → separable_element K x → separable_element E x.
Lemma adjoin_separableP {
K x} :
-
reflect (
∀ y,
y \in <<K; x>>%
VS → separable_element K y)
+
reflect (
∀ y,
y \in <<K; x>>%
VS → separable_element K y)
(
separable_element K x).
Lemma separable_exponent K x :
-
∃ n, [char L].-nat n && separable_element K (
x ^+ n).
+
∃ n, [char L].-nat n && separable_element K (
x ^+ n).
-
Lemma charf0_separable K :
[char L] =i pred0 → ∀ x,
separable_element K x.
+
Lemma charf0_separable K :
[char L] =i pred0 → ∀ x,
separable_element K x.
Lemma charf_p_separable K x e p :
-
p \in [char L] → separable_element K x = (x \in <<K; x ^+ (p ^ e.+1)>>%
VS).
+
p \in [char L] → separable_element K x = (x \in <<K; x ^+ (p ^ e.+1)>>%
VS).
Lemma charf_n_separable K x n :
-
[char L].-nat n → 1
< n → separable_element K x = (x \in <<K; x ^+ n>>%
VS).
+
[char L].-nat n → 1
< n → separable_element K x = (x \in <<K; x ^+ n>>%
VS).
Definition purely_inseparable_element U x :=
-
x ^+ ex_minn (
separable_exponent <<U>> x)
\in U.
+
x ^+ ex_minn (
separable_exponent <<U>> x)
\in U.
Lemma purely_inseparable_elementP {
K x} :
-
reflect (
exists2 n, [char L].-nat n & x ^+ n \in K)
+
reflect (
exists2 n, [char L].-nat n & x ^+ n \in K)
(
purely_inseparable_element K x).
Lemma separable_inseparable_element K x :
-
separable_element K x && purely_inseparable_element K x = (x \in K).
+
separable_element K x && purely_inseparable_element K x = (x \in K).
-
Lemma base_inseparable K x :
x \in K → purely_inseparable_element K x.
+
Lemma base_inseparable K x :
x \in K → purely_inseparable_element K x.
Lemma sub_inseparable K E x :
- (
K ≤ E)%
VS → purely_inseparable_element K x →
+ (
K ≤ E)%
VS → purely_inseparable_element K x →
purely_inseparable_element E x.
Section PrimitiveElementTheorem.
-
Variables (
K :
{subfield L}) (
x y :
L).
+
Variables (
K :
{subfield L}) (
x y :
L).
Section FiniteCase.
-
Variable N :
nat.
+
Variable N :
nat.
-
Let K_is_large :=
∃ s, [/\ uniq s, {subset s ≤ K} & N < size s].
+
Let K_is_large :=
∃ s, [/\ uniq s, {subset s ≤ K} & N < size s].
-
Let cyclic_or_large (
z :
L) :
z != 0
→ K_is_large ∨ ∃ a, z ^+ a.+1 = 1.
+
Let cyclic_or_large (
z :
L) :
z != 0
→ K_is_large ∨ ∃ a, z ^+ a.+1 = 1.
-
Lemma finite_PET :
K_is_large ∨ ∃ z, (
<< <<K; y>>; x>> = <<K; z>>)%
VS.
+
Lemma finite_PET :
K_is_large ∨ ∃ z, (
<< <<K; y>>; x>> = <<K; z>>)%
VS.
End FiniteCase.
@@ -379,112 +378,112 @@ http://www.math.uconn.edu/~kconrad/blurbs/galoistheory/separable2.pdf
Hypothesis sepKy :
separable_element K y.
-
Lemma Primitive_Element_Theorem :
∃ z, (
<< <<K; y>>; x>> = <<K; z>>)%
VS.
+
Lemma Primitive_Element_Theorem :
∃ z, (
<< <<K; y>>; x>> = <<K; z>>)%
VS.
-
Lemma adjoin_separable :
separable_element <<K; y>> x → separable_element K x.
+
Lemma adjoin_separable :
separable_element <<K; y>> x → separable_element K x.
End PrimitiveElementTheorem.
Lemma strong_Primitive_Element_Theorem K x y :
-
separable_element <<K; x>> y →
-
exists2 z : L, (
<< <<K; y>>; x>> = <<K; z>>)%
VS
-
& separable_element K x → separable_element K y.
+
separable_element <<K; x>> y →
+
exists2 z : L, (
<< <<K; y>>; x>> = <<K; z>>)%
VS
+
& separable_element K x → separable_element K y.
-
Definition separable U W :
bool :=
+
Definition separable U W :
bool :=
all (
separable_element U) (
vbasis W).
-
Definition purely_inseparable U W :
bool :=
+
Definition purely_inseparable U W :
bool :=
all (
purely_inseparable_element U) (
vbasis W).
Lemma separable_add K x y :
-
separable_element K x → separable_element K y → separable_element K (
x + y).
+
separable_element K x → separable_element K y → separable_element K (
x + y).
-
Lemma separable_sum I r (
P :
pred I) (
v_ :
I → L)
K :
-
(∀ i,
P i → separable_element K (
v_ i)
) →
-
separable_element K (
\sum_(i <- r | P i) v_ i).
+
Lemma separable_sum I r (
P :
pred I) (
v_ :
I → L)
K :
+
(∀ i,
P i → separable_element K (
v_ i)
) →
+
separable_element K (
\sum_(i <- r | P i) v_ i).
Lemma inseparable_add K x y :
-
purely_inseparable_element K x → purely_inseparable_element K y →
-
purely_inseparable_element K (
x + y).
+
purely_inseparable_element K x → purely_inseparable_element K y →
+
purely_inseparable_element K (
x + y).
-
Lemma inseparable_sum I r (
P :
pred I) (
v_ :
I → L)
K :
-
(∀ i,
P i → purely_inseparable_element K (
v_ i)
) →
-
purely_inseparable_element K (
\sum_(i <- r | P i) v_ i).
+
Lemma inseparable_sum I r (
P :
pred I) (
v_ :
I → L)
K :
+
(∀ i,
P i → purely_inseparable_element K (
v_ i)
) →
+
purely_inseparable_element K (
\sum_(i <- r | P i) v_ i).
Lemma separableP {
K E} :
-
reflect (
∀ y,
y \in E → separable_element K y) (
separable K E).
+
reflect (
∀ y,
y \in E → separable_element K y) (
separable K E).
Lemma purely_inseparableP {
K E} :
-
reflect (
∀ y,
y \in E → purely_inseparable_element K y)
+
reflect (
∀ y,
y \in E → purely_inseparable_element K y)
(
purely_inseparable K E).
-
Lemma adjoin_separable_eq K x :
separable_element K x = separable K <<K; x>>%
VS.
+
Lemma adjoin_separable_eq K x :
separable_element K x = separable K <<K; x>>%
VS.
Lemma separable_inseparable_decomposition E K :
-
{x | x \in E ∧ separable_element K x & purely_inseparable <<K; x>> E}.
+
{x | x \in E ∧ separable_element K x & purely_inseparable <<K; x>> E}.
Definition separable_generator K E :
L :=
-
s2val (
locked (
separable_inseparable_decomposition E K)).
+
s2val (
locked (
separable_inseparable_decomposition E K)).
-
Lemma separable_generator_mem E K :
separable_generator K E \in E.
+
Lemma separable_generator_mem E K :
separable_generator K E \in E.
Lemma separable_generatorP E K :
separable_element K (
separable_generator K E).
Lemma separable_generator_maximal E K :
-
purely_inseparable <<K; separable_generator K E>> E.
+
purely_inseparable <<K; separable_generator K E>> E.
Lemma sub_adjoin_separable_generator E K :
-
separable K E → (
E ≤ <<K; separable_generator K E>>)%
VS.
+
separable K E → (
E ≤ <<K; separable_generator K E>>)%
VS.
Lemma eq_adjoin_separable_generator E K :
-
separable K E → (
K ≤ E)%
VS →
-
E = <<K; separable_generator K E>>%
VS :> {vspace _}.
+
separable K E → (
K ≤ E)%
VS →
+
E = <<K; separable_generator K E>>%
VS :> {vspace _}.
Lemma separable_refl K :
separable K K.
-
Lemma separable_trans M K E :
separable K M → separable M E → separable K E.
+
Lemma separable_trans M K E :
separable K M → separable M E → separable K E.
Lemma separableS K1 K2 E2 E1 :
- (
K1 ≤ K2)%
VS → (
E2 ≤ E1)%
VS → separable K1 E1 → separable K2 E2.
+ (
K1 ≤ K2)%
VS → (
E2 ≤ E1)%
VS → separable K1 E1 → separable K2 E2.
-
Lemma separableSl K M E : (
K ≤ M)%
VS → separable K E → separable M E.
+
Lemma separableSl K M E : (
K ≤ M)%
VS → separable K E → separable M E.
-
Lemma separableSr K M E : (
M ≤ E)%
VS → separable K E → separable K M.
+
Lemma separableSr K M E : (
M ≤ E)%
VS → separable K E → separable K M.
Lemma separable_Fadjoin_seq K rs :
-
all (
separable_element K)
rs → separable K <<K & rs>>.
+
all (
separable_element K)
rs → separable K <<K & rs>>.
Lemma purely_inseparable_refl K :
purely_inseparable K K.
Lemma purely_inseparable_trans M K E :
-
purely_inseparable K M → purely_inseparable M E → purely_inseparable K E.
+
purely_inseparable K M → purely_inseparable M E → purely_inseparable K E.
End Separable.
--
cgit v1.2.3