English
If there exists an F-basis of A whose image is linearly independent over L, then A and L are linearly disjoint.
Русский
Если существует F-базис A, образ которого линейно независим над L, то A и L линейно разобщены.
LaTeX
$$$\exists \text{Basis } a \,\text{of } A\; (\mathrm{LinearIndependent}_L(A_{\mathrm{val}} \circ a)) \Rightarrow A \perp_F L$$$
Lean4
/-- If there exists an `F`-basis of `A` which remains linearly independent over `L`, then
`A` and `L` are linearly disjoint. -/
theorem of_basis_left {ι : Type*} (a : Basis ι F A) (H : LinearIndependent L (A.val ∘ a)) : A.LinearDisjoint L :=
Subalgebra.LinearDisjoint.of_basis_left _ _ a <|
H.map_of_surjective_injective (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) (AddMonoidHom.id E)
(AlgEquiv.surjective _) (by simp) (fun _ _ ↦ by simp_rw [Algebra.smul_def]; rfl)
