English
A version of the previous criterion allowing abstract fields; if A is linearly disjoint from L, then for any L′ with a tower structure, A is linearly disjoint from L′.
Русский
Версия предыдущего критерия для абстрактных полей; если A линейно разобщено с L, то для любых расширений L′ над F, A линейно разобщено с L′.
LaTeX
$$$A \perp_F L \Rightarrow A \perp_F L'\text{ for suitable extensions }L'$$$
Lean4
/-- If `A` and `L` are linearly disjoint, then any `F`-linearly independent family on `L` remains
linearly independent over `A`. -/
theorem linearIndependent_right' (H : A.LinearDisjoint L) {ι : Type*} {b : ι → L} (hb : LinearIndependent F b) :
LinearIndependent A (algebraMap L E ∘ b) := by
apply
Subalgebra.LinearDisjoint.linearIndependent_right_of_flat H <|
hb.map' _ (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toLinearEquiv.ker
