theorem
isSeparable_iff_exists_monic_irreducible_separable
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
[FiniteDimensional K L]
:
Algebra.IsSeparable K L ↔ ∃ (f : Polynomial K), f.Monic ∧ Irreducible f ∧ f.Separable ∧ Nonempty (L ≃ₐ[K] AdjoinRoot f)
theorem
finSepDegree_le_finrank_and_eq_iff_separable
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
[FiniteDimensional K L]
:
Field.finSepDegree K L ≤ Module.finrank K L ∧ (Field.finSepDegree K L = Module.finrank K L ↔ Algebra.IsSeparable K L)
theorem
isSeparable_tower_iff_of_finiteDimensional
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
{F : Type u_3}
[Field F]
[Algebra K F]
[Algebra F L]
[IsScalarTower K F L]
[FiniteDimensional K L]
[FiniteDimensional K F]
[FiniteDimensional F L]
:
theorem
separableClosure_isSeparable
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
:
Algebra.IsSeparable K ↥(separableClosure K L)