English
If A is linearly disjoint from L over F and a is an F-linearly independent family in A, then the image of a in E (via the inclusion A → E) is L-linearly independent in E.
Русский
Пусть A линейно разобщено с L над F, и {a_i} — F-линейно независимая семейство в A. Образ этой семейства в E через включение A → E линейно независим над L в E.
LaTeX
$$$A \perp_F L \;\Rightarrow\; \forall \iota\, (a:\iota \to A),\; \mathrm{LinearIndependent}_F(a) \Rightarrow \mathrm{LinearIndependent}_L(A_{\mathrm{val}} \circ a).$$$
Lean4
/-- If `A` and `L` are linearly disjoint, then any `F`-linearly independent family on `A` remains
linearly independent over `L`. -/
theorem linearIndependent_left (H : A.LinearDisjoint L) {ι : Type*} {a : ι → A} (ha : LinearIndependent F a) :
LinearIndependent L (A.val ∘ a) :=
(Subalgebra.LinearDisjoint.linearIndependent_left_of_flat H ha).map_of_injective_injective
(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) (AddMonoidHom.id E) (by simp) (by simp)
(fun _ _ ↦ by simp_rw [Algebra.smul_def]; rfl)
