theorem EtaleAlgebras.separable_polynomial_def {K : Type u_1} [CommSemiring K] (f : Polynomial K) : f.Separable ↔ IsCoprime f (Polynomial.derivative f)

theorem EtaleAlgebras.isSeparable_extension_def (F : Type u_1) (K : Type u_2) [CommRing F] [Ring K] [Algebra F K] : Algebra.IsSeparable F K ↔ ∀ (x : K), IsSeparable F x

theorem EtaleAlgebras.irreducible_not_separable_iff_derivative_eq_zero {K : Type u_1} [Field K] {f : Polynomial K} (hf : Irreducible f) : ¬f.Separable ↔ Polynomial.derivative f = 0

theorem irreducible_eq_expand_separable {K : Type u_1} [Field K] {f : Polynomial K} (hf : Irreducible f) : ∃ (n : ℕ) (g : Polynomial K), Irreducible g ∧ g.Separable ∧ (Polynomial.expand K (ringChar K ^ n)) g = f

theorem isSeparable_of_charZero_of_isAlgebraic (K : Type u_1) [Field K] [CharZero K] (L : Type u_2) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] : Algebra.IsSeparable K L

theorem algHom_card_eq_roots (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] {α : L} (halg : IsAlgebraic K α) : Field.finSepDegree K ↥K⟮α⟯ = (minpoly K α).natSepDegree

theorem algHom_card_le_finrank (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] {α : L} (halg : IsAlgebraic K α) : Field.finSepDegree K ↥K⟮α⟯ ≤ Module.finrank K ↥K⟮α⟯

theorem algHom_card_eq_finrank_iff_separable (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] {α : L} (halg : IsAlgebraic K α) : Field.finSepDegree K ↥K⟮α⟯ = Module.finrank K ↥K⟮α⟯ ↔ IsSeparable K α

theorem algHom_card_properties (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] {α : L} (halg : IsAlgebraic K α) : Field.finSepDegree K ↥K⟮α⟯ = (minpoly K α).natSepDegree ∧ Field.finSepDegree K ↥K⟮α⟯ ≤ Module.finrank K ↥K⟮α⟯ ∧ (Field.finSepDegree K ↥K⟮α⟯ = Module.finrank K ↥K⟮α⟯ ↔ IsSeparable K α)

theorem separable_degree_def (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : Field.finSepDegree K L = Nat.card (Field.Emb K L)

theorem exists_ringHom_extension_of_isAlgClosed (K : Type u_1) (L : Type u_2) (Ω : Type u_3) [Field K] [Field L] [Field Ω] [Algebra K L] [Algebra.IsAlgebraic K L] [IsAlgClosed Ω] (φ_K : K →+* Ω) : ∃ (φ_L : L →+* Ω), φ_L.comp (algebraMap K L) = φ_K

theorem mem_separableClosure_iff_isSeparable (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] (x : L) : x ∈ separableClosure K L ↔ IsSeparable K x

theorem algebraic_isSeparable_of_perfectField (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [PerfectField K] : Algebra.IsSeparable K L

theorem perfectField_iff_frobenius_surjective (K : Type u_1) [Field K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : PerfectField K ↔ Function.Surjective ⇑(frobenius K p)

theorem finiteField_perfectField (K : Type u_1) [Field K] [Finite K] : PerfectField K

theorem sepClosed_iff_splits_separable (K : Type u_1) [Field K] : IsSepClosed K ↔ ∀ (f : Polynomial K), f.Separable → f.Splits

theorem isPurelyInseparable_iff_finSepDegree (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : IsPurelyInseparable K L ↔ Field.finSepDegree K L = 1

theorem hom_count_mul_tower (K' : Type u) (F : Type v) (L : Type w) [Field K'] [Field F] [Field L] [Algebra K' F] [Algebra K' L] [Algebra F L] [IsScalarTower K' F L] [FiniteDimensional K' F] [FiniteDimensional F L] : Field.finSepDegree K' F * Field.finSepDegree F L = Field.finSepDegree K' L

theorem separable_degree_mul_tower (K' : Type u) (F : Type v) (L : Type w) [Field K'] [Field F] [Field L] [Algebra K' F] [Algebra K' L] [Algebra F L] [IsScalarTower K' F L] [FiniteDimensional K' F] [FiniteDimensional F L] : Field.finSepDegree K' F * Field.finSepDegree F L = Field.finSepDegree K' L

theorem purelyInseparable_prime_degree_structure (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] [IsPurelyInseparable K L] [FiniteDimensional K L] (hdeg : Module.finrank K L = p) : ∃ (α : L) (a : K), minpoly K α = Polynomial.X ^ p - Polynomial.C a ∧ (∀ (b : K), b ^ p ≠ a) ∧ K⟮α⟯ = ⊤

theorem separableClosure_isPurelyInseparable (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] : IsPurelyInseparable (↥(separableClosure K L)) L

theorem separableClosure_decomposition (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] : Algebra.IsSeparable K ↥(separableClosure K L) ∧ IsPurelyInseparable (↥(separableClosure K L)) L ∧ ∀ (F : IntermediateField K L), Algebra.IsSeparable K ↥F → IsPurelyInseparable (↥F) L → F = separableClosure K L

theorem finInsepDegree_eq_expChar_pow (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (q : ℕ) [ExpChar K q] : ∃ (n : ℕ), Field.finInsepDegree K L = q ^ n

theorem etale_base_change (K : Type u_1) (K' : Type u_2) [Field K] [Field K'] [Algebra K K'] (L : Type u_3) [CommRing L] [Algebra K L] [Algebra.Etale K L] [Module.Finite K L] : Algebra.Etale K' (TensorProduct K K' L)

theorem etale_finite_base_change (K : Type u_1) (K' : Type u_2) [Field K] [Field K'] [Algebra K K'] (L : Type u_3) [CommRing L] [Algebra K L] [Algebra.Etale K L] [Module.Finite K L] : Module.Finite K' (TensorProduct K K' L)

theorem etale_base_change_finrank_eq (K : Type u_1) (K' : Type u_2) [Field K] [Field K'] [Algebra K K'] (L : Type u_3) [CommRing L] [Algebra K L] [Algebra.Etale K L] [Module.Finite K L] : Module.finrank K L = Module.finrank K' (TensorProduct K K' L)

theorem etale_base_change_bundle (K : Type u_1) (K' : Type u_2) [Field K] [Field K'] [Algebra K K'] (L : Type u_3) [CommRing L] [Algebra K L] [Algebra.Etale K L] [Module.Finite K L] : Algebra.Etale K' (TensorProduct K K' L) ∧ Module.Finite K' (TensorProduct K K' L) ∧ Module.finrank K L = Module.finrank K' (TensorProduct K K' L)

theorem semisimple_iff_reduced (K : Type u_1) [Field K] (A : Type u_2) [CommRing A] [Algebra K A] [Module.Finite K A] : IsSemisimpleRing A ↔ IsReduced A