Library mathcomp.field.separable
- -
-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-
-
-- Distributed under the terms of CeCILL-B. *)
- -
-
- This file provides a theory of separable and inseparable field extensions.
-
-
-
- separable_poly p <=> p has no multiple roots in any field extension.
- separable_element K x <=> the minimal polynomial of x over K is separable.
- separable K E <=> every member of E is separable over K.
- separable_generator K E == some x \in E that generates the largest
- subfield K[x] that is separable over K.
- purely_inseparable_element K x <=> there is a [char L].-nat n such that
- x ^+ n \in K.
- purely_inseparable K E <=> every member of E is purely inseparable over K.
-
-
-
- Derivations are introduced to prove the adjoin_separableP Lemma:
- Derivation K D <=> the linear operator D satifies the Leibniz
- product rule inside K.
- extendDerivation x D K == given a derivation D on K and a separable
- element x over K, this function returns the
- unique extension of D to K(x).
-
-
-
-
-Set Implicit Arguments.
- -
-Local Open Scope ring_scope.
-Import GRing.Theory.
- -
-Section SeparablePoly.
- -
-Variable R : idomainType.
-Implicit Types p q d u v : {poly R}.
- -
-Definition separable_poly p := coprimep p p^`.
- -
- -
-Lemma separable_poly_neq0 p : separable p → p != 0.
- -
-Lemma poly_square_freeP p :
- (∀ u v, u × v %| p → coprimep u v)
- ↔ (∀ u, size u != 1%N → ~~ (u ^+ 2 %| p)).
- -
-Lemma separable_polyP {p} :
- reflect [/\ ∀ u v, u × v %| p → coprimep u v
- & ∀ u, u %| p → 1 < size u → u^` != 0]
- (separable p).
- -
-Lemma separable_coprime p u v : separable p → u × v %| p → coprimep u v.
- -
-Lemma separable_nosquare p u k :
- separable p → 1 < k → size u != 1%N → (u ^+ k %| p) = false.
- -
-Lemma separable_deriv_eq0 p u :
- separable p → u %| p → 1 < size u → (u^` == 0) = false.
- -
-Lemma dvdp_separable p q : q %| p → separable p → separable q.
- -
-Lemma separable_mul p q :
- separable (p × q) = [&& separable p, separable q & coprimep p q].
- -
-Lemma eqp_separable p q : p %= q → separable p = separable q.
- -
-Lemma separable_root p x :
- separable (p × ('X - x%:P)) = separable p && ~~ root p x.
- -
-Lemma separable_prod_XsubC (r : seq R) :
- separable (\prod_(x <- r) ('X - x%:P)) = uniq r.
- -
-Lemma make_separable p : p != 0 → separable (p %/ gcdp p p^`).
- -
-End SeparablePoly.
- -
- -
-Lemma separable_map (F : fieldType) (R : idomainType)
- (f : {rmorphism F → R}) (p : {poly F}) :
- separable_poly (map_poly f p) = separable_poly p.
- -
-Section InfinitePrimitiveElementTheorem.
- -
- -
-Variables (F L : fieldType) (iota : {rmorphism F → L}).
-Variables (x y : L) (p : {poly F}).
-Hypotheses (nz_p : p != 0) (px_0 : root (p ^ iota) x).
- -
-Let inFz z w := ∃ q, (q ^ iota).[z] = w.
- -
-Lemma large_field_PET q :
- root (q ^ iota) y → separable_poly q →
- exists2 r, r != 0
- & ∀ t (z := iota t × y - x), ~~ root r (iota t) → inFz z x ∧ inFz z y.
- -
-Lemma char0_PET (q : {poly F}) :
- q != 0 → root (q ^ iota) y → [char F] =i pred0 →
- ∃ n, let z := y *+ n - x in inFz z x ∧ inFz z y.
- -
-End InfinitePrimitiveElementTheorem.
- -
-Section Separable.
- -
-Variables (F : fieldType) (L : fieldExtType F).
-Implicit Types (U V W : {vspace L}) (E K M : {subfield L}) (D : 'End(L)).
- -
-Section Derivation.
- -
-Variables (K : {vspace L}) (D : 'End(L)).
- -
-
-
--Set Implicit Arguments.
- -
-Local Open Scope ring_scope.
-Import GRing.Theory.
- -
-Section SeparablePoly.
- -
-Variable R : idomainType.
-Implicit Types p q d u v : {poly R}.
- -
-Definition separable_poly p := coprimep p p^`.
- -
- -
-Lemma separable_poly_neq0 p : separable p → p != 0.
- -
-Lemma poly_square_freeP p :
- (∀ u v, u × v %| p → coprimep u v)
- ↔ (∀ u, size u != 1%N → ~~ (u ^+ 2 %| p)).
- -
-Lemma separable_polyP {p} :
- reflect [/\ ∀ u v, u × v %| p → coprimep u v
- & ∀ u, u %| p → 1 < size u → u^` != 0]
- (separable p).
- -
-Lemma separable_coprime p u v : separable p → u × v %| p → coprimep u v.
- -
-Lemma separable_nosquare p u k :
- separable p → 1 < k → size u != 1%N → (u ^+ k %| p) = false.
- -
-Lemma separable_deriv_eq0 p u :
- separable p → u %| p → 1 < size u → (u^` == 0) = false.
- -
-Lemma dvdp_separable p q : q %| p → separable p → separable q.
- -
-Lemma separable_mul p q :
- separable (p × q) = [&& separable p, separable q & coprimep p q].
- -
-Lemma eqp_separable p q : p %= q → separable p = separable q.
- -
-Lemma separable_root p x :
- separable (p × ('X - x%:P)) = separable p && ~~ root p x.
- -
-Lemma separable_prod_XsubC (r : seq R) :
- separable (\prod_(x <- r) ('X - x%:P)) = uniq r.
- -
-Lemma make_separable p : p != 0 → separable (p %/ gcdp p p^`).
- -
-End SeparablePoly.
- -
- -
-Lemma separable_map (F : fieldType) (R : idomainType)
- (f : {rmorphism F → R}) (p : {poly F}) :
- separable_poly (map_poly f p) = separable_poly p.
- -
-Section InfinitePrimitiveElementTheorem.
- -
- -
-Variables (F L : fieldType) (iota : {rmorphism F → L}).
-Variables (x y : L) (p : {poly F}).
-Hypotheses (nz_p : p != 0) (px_0 : root (p ^ iota) x).
- -
-Let inFz z w := ∃ q, (q ^ iota).[z] = w.
- -
-Lemma large_field_PET q :
- root (q ^ iota) y → separable_poly q →
- exists2 r, r != 0
- & ∀ t (z := iota t × y - x), ~~ root r (iota t) → inFz z x ∧ inFz z y.
- -
-Lemma char0_PET (q : {poly F}) :
- q != 0 → root (q ^ iota) y → [char F] =i pred0 →
- ∃ n, let z := y *+ n - x in inFz z x ∧ inFz z y.
- -
-End InfinitePrimitiveElementTheorem.
- -
-Section Separable.
- -
-Variables (F : fieldType) (L : fieldExtType F).
-Implicit Types (U V W : {vspace L}) (E K M : {subfield L}) (D : 'End(L)).
- -
-Section Derivation.
- -
-Variables (K : {vspace L}) (D : 'End(L)).
- -
-
- A deriviation only needs to be additive and satify Lebniz's law, but all
- the deriviations used here are going to be linear, so we only define
- the Derivation predicate for linear endomorphisms.
-
-
-Definition Derivation (s := vbasis K) : bool :=
- all (fun u ⇒ all (fun v ⇒ D (u × v) == D u × v + u × D v) s) s.
- -
-Hypothesis derD : Derivation.
- -
-Lemma Derivation_mul : {in K &, ∀ u v, D (u × v) = D u × v + u × D v}.
- -
-Lemma Derivation_mul_poly (Dp := map_poly D) :
- {in polyOver K &, ∀ p q, Dp (p × q) = Dp p × q + p × Dp q}.
- -
-End Derivation.
- -
-Lemma DerivationS E K D : (K ≤ E)%VS → Derivation E D → Derivation K D.
- -
-Section DerivationAlgebra.
- -
-Variables (E : {subfield L}) (D : 'End(L)).
-Hypothesis derD : Derivation E D.
- -
-Lemma Derivation1 : D 1 = 0.
- -
-Lemma Derivation_scalar x : x \in 1%VS → D x = 0.
- -
-Lemma Derivation_exp x m : x \in E → D (x ^+ m) = x ^+ m.-1 *+ m × D x.
- -
-Lemma Derivation_horner p x :
- p \is a polyOver E → x \in E →
- D p.[x] = (map_poly D p).[x] + p^`.[x] × D x.
- -
-End DerivationAlgebra.
- -
-Definition separable_element U x := separable_poly (minPoly U x).
- -
-Section SeparableElement.
- -
-Variables (K : {subfield L}) (x : L).
- -
-Lemma separable_elementP :
- reflect (∃ f, [/\ f \is a polyOver K, root f x & separable_poly f])
- (separable_element K x).
- -
-Lemma base_separable : x \in K → separable_element K x.
- -
-Lemma separable_nz_der : separable_element K x = ((minPoly K x)^` != 0).
- -
-Lemma separablePn :
- reflect (exists2 p, p \in [char L] &
- exists2 g, g \is a polyOver K & minPoly K x = g \Po 'X^p)
- (~~ separable_element K x).
- -
-Lemma separable_root_der : separable_element K x (+) root (minPoly K x)^` x.
- -
-Lemma Derivation_separable D :
- Derivation <<K; x>> D → separable_element K x →
- D x = - (map_poly D (minPoly K x)).[x] / (minPoly K x)^`.[x].
- -
-Section ExtendDerivation.
- -
-Variable D : 'End(L).
- -
-Let Dx E := - (map_poly D (minPoly E x)).[x] / ((minPoly E x)^`).[x].
- -
-Fact extendDerivation_subproof E (adjEx := Fadjoin_poly E x) :
- let body y (p := adjEx y) := (map_poly D p).[x] + p^`.[x] × Dx E in
- linear body.
- -
-Definition extendDerivation E : 'End(L) :=
- linfun (Linear (extendDerivation_subproof E)).
- -
-Hypothesis derD : Derivation K D.
- -
-Lemma extendDerivation_id y : y \in K → extendDerivation K y = D y.
- -
-Lemma extendDerivation_horner p :
- p \is a polyOver K → separable_element K x →
- extendDerivation K p.[x] = (map_poly D p).[x] + p^`.[x] × Dx K.
- -
-Lemma extendDerivationP :
- separable_element K x → Derivation <<K; x>> (extendDerivation K).
- -
-End ExtendDerivation.
- -
-
-
-- all (fun u ⇒ all (fun v ⇒ D (u × v) == D u × v + u × D v) s) s.
- -
-Hypothesis derD : Derivation.
- -
-Lemma Derivation_mul : {in K &, ∀ u v, D (u × v) = D u × v + u × D v}.
- -
-Lemma Derivation_mul_poly (Dp := map_poly D) :
- {in polyOver K &, ∀ p q, Dp (p × q) = Dp p × q + p × Dp q}.
- -
-End Derivation.
- -
-Lemma DerivationS E K D : (K ≤ E)%VS → Derivation E D → Derivation K D.
- -
-Section DerivationAlgebra.
- -
-Variables (E : {subfield L}) (D : 'End(L)).
-Hypothesis derD : Derivation E D.
- -
-Lemma Derivation1 : D 1 = 0.
- -
-Lemma Derivation_scalar x : x \in 1%VS → D x = 0.
- -
-Lemma Derivation_exp x m : x \in E → D (x ^+ m) = x ^+ m.-1 *+ m × D x.
- -
-Lemma Derivation_horner p x :
- p \is a polyOver E → x \in E →
- D p.[x] = (map_poly D p).[x] + p^`.[x] × D x.
- -
-End DerivationAlgebra.
- -
-Definition separable_element U x := separable_poly (minPoly U x).
- -
-Section SeparableElement.
- -
-Variables (K : {subfield L}) (x : L).
- -
-Lemma separable_elementP :
- reflect (∃ f, [/\ f \is a polyOver K, root f x & separable_poly f])
- (separable_element K x).
- -
-Lemma base_separable : x \in K → separable_element K x.
- -
-Lemma separable_nz_der : separable_element K x = ((minPoly K x)^` != 0).
- -
-Lemma separablePn :
- reflect (exists2 p, p \in [char L] &
- exists2 g, g \is a polyOver K & minPoly K x = g \Po 'X^p)
- (~~ separable_element K x).
- -
-Lemma separable_root_der : separable_element K x (+) root (minPoly K x)^` x.
- -
-Lemma Derivation_separable D :
- Derivation <<K; x>> D → separable_element K x →
- D x = - (map_poly D (minPoly K x)).[x] / (minPoly K x)^`.[x].
- -
-Section ExtendDerivation.
- -
-Variable D : 'End(L).
- -
-Let Dx E := - (map_poly D (minPoly E x)).[x] / ((minPoly E x)^`).[x].
- -
-Fact extendDerivation_subproof E (adjEx := Fadjoin_poly E x) :
- let body y (p := adjEx y) := (map_poly D p).[x] + p^`.[x] × Dx E in
- linear body.
- -
-Definition extendDerivation E : 'End(L) :=
- linfun (Linear (extendDerivation_subproof E)).
- -
-Hypothesis derD : Derivation K D.
- -
-Lemma extendDerivation_id y : y \in K → extendDerivation K y = D y.
- -
-Lemma extendDerivation_horner p :
- p \is a polyOver K → separable_element K x →
- extendDerivation K p.[x] = (map_poly D p).[x] + p^`.[x] × Dx K.
- -
-Lemma extendDerivationP :
- separable_element K x → Derivation <<K; x>> (extendDerivation K).
- -
-End ExtendDerivation.
- -
-
- Reference:
-http://www.math.uconn.edu/~kconrad/blurbs/galoistheory/separable2.pdf
-
-
-Lemma Derivation_separableP :
- reflect
- (∀ D, Derivation <<K; x>> D → K ≤ lker D → <<K; x>> ≤ lker D)%VS
- (separable_element K x).
- -
-End SeparableElement.
- -
- -
-Lemma separable_elementS K 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)
- (separable_element K x).
- -
-Lemma separable_exponent K x :
- ∃ n, [char L].-nat n && separable_element K (x ^+ n).
- -
-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).
- -
-Lemma charf_n_separable K x n :
- [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.
- -
-Lemma purely_inseparable_elementP {K x} :
- 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).
- -
-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 →
- purely_inseparable_element E x.
- -
-Section PrimitiveElementTheorem.
- -
-Variables (K : {subfield L}) (x y : L).
- -
-Section FiniteCase.
- -
-Variable N : nat.
- -
-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.
- -
-Lemma finite_PET : K_is_large ∨ ∃ z, (<< <<K; y>>; x>> = <<K; z>>)%VS.
- -
-End FiniteCase.
- -
-Hypothesis sepKy : separable_element K y.
- -
-Lemma Primitive_Element_Theorem : ∃ z, (<< <<K; y>>; x>> = <<K; z>>)%VS.
- -
-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.
- -
-Definition separable U W : bool :=
- all (separable_element U) (vbasis W).
- -
-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).
- -
-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).
- -
-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).
- -
-Lemma purely_inseparableP {K E} :
- 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 separable_inseparable_decomposition E K :
- {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)).
- -
-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.
- -
-Lemma sub_adjoin_separable_generator E K :
- 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 _}.
- -
-Lemma separable_refl K : separable K K.
- -
-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.
- -
-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 separable_Fadjoin_seq 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.
- -
-End Separable.
- -
-
-- reflect
- (∀ D, Derivation <<K; x>> D → K ≤ lker D → <<K; x>> ≤ lker D)%VS
- (separable_element K x).
- -
-End SeparableElement.
- -
- -
-Lemma separable_elementS K 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)
- (separable_element K x).
- -
-Lemma separable_exponent K x :
- ∃ n, [char L].-nat n && separable_element K (x ^+ n).
- -
-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).
- -
-Lemma charf_n_separable K x n :
- [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.
- -
-Lemma purely_inseparable_elementP {K x} :
- 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).
- -
-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 →
- purely_inseparable_element E x.
- -
-Section PrimitiveElementTheorem.
- -
-Variables (K : {subfield L}) (x y : L).
- -
-Section FiniteCase.
- -
-Variable N : nat.
- -
-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.
- -
-Lemma finite_PET : K_is_large ∨ ∃ z, (<< <<K; y>>; x>> = <<K; z>>)%VS.
- -
-End FiniteCase.
- -
-Hypothesis sepKy : separable_element K y.
- -
-Lemma Primitive_Element_Theorem : ∃ z, (<< <<K; y>>; x>> = <<K; z>>)%VS.
- -
-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.
- -
-Definition separable U W : bool :=
- all (separable_element U) (vbasis W).
- -
-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).
- -
-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).
- -
-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).
- -
-Lemma purely_inseparableP {K E} :
- 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 separable_inseparable_decomposition E K :
- {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)).
- -
-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.
- -
-Lemma sub_adjoin_separable_generator E K :
- 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 _}.
- -
-Lemma separable_refl K : separable K K.
- -
-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.
- -
-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 separable_Fadjoin_seq 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.
- -
-End Separable.
- -
-