English
If E/F and K/E are purely inseparable, then K/F is purely inseparable.
Русский
Если E/F и K/E чисто безразделимы, то K/F тоже чисто безразделимо.
LaTeX
$$$ IsPurelyInseparable(F,E) \land IsPurelyInseparable(E,K) \Rightarrow IsPurelyInseparable(F,K) $$$
Lean4
/-- If `E / F` and `K / E` are both purely inseparable extensions, then `K / F` is also
purely inseparable. -/
@[stacks 02JJ "See also 00GM"]
theorem trans [Algebra E K] [IsScalarTower F E K] [h1 : IsPurelyInseparable F E] [h2 : IsPurelyInseparable E K] :
IsPurelyInseparable F K := by
obtain ⟨q, _⟩ := ExpChar.exists F
haveI := expChar_of_injective_algebraMap (algebraMap F E).injective q
rw [isPurelyInseparable_iff_pow_mem _ q] at h1 h2 ⊢
intro x
obtain ⟨n, y, h2⟩ := h2 x
obtain ⟨m, z, h1⟩ := h1 y
refine ⟨n + m, z, ?_⟩
rw [IsScalarTower.algebraMap_apply F E K, h1, map_pow, h2, ← pow_mul, ← pow_add]
