English
If finSepDegree F E = 1, then E/F is purely inseparable.
Русский
Если finSepDegree F E = 1, то E/F чисто безразделимо.
LaTeX
$$$ finSepDegree F E = 1 \Rightarrow IsPurelyInseparable F E $$$
Lean4
/-- If an extension has finite separable degree one, then it is purely inseparable. -/
theorem isPurelyInseparable_of_finSepDegree_eq_one (hdeg : finSepDegree F E = 1) : IsPurelyInseparable F E :=
by
by_cases H : Algebra.IsAlgebraic F E
· rw [isPurelyInseparable_iff]
refine fun x ↦ ⟨Algebra.IsIntegral.isIntegral x, fun hsep ↦ ?_⟩
have := finSepDegree_mul_finSepDegree_of_isAlgebraic F F⟮x⟯ E
rw [hdeg, mul_eq_one, (finSepDegree_adjoin_simple_eq_finrank_iff F E x (Algebra.IsAlgebraic.isAlgebraic x)).2 hsep,
IntermediateField.finrank_eq_one_iff] at this
simpa only [this.1] using mem_adjoin_simple_self F x
· rw [← Algebra.transcendental_iff_not_isAlgebraic] at H
simp [finSepDegree_eq_zero_of_transcendental F E] at hdeg
