English
If A and B are linearly disjoint, then the family formed by products a_i b_j with a_i from A and b_j from B is F-linearly independent.
Русский
Если A и B линейно разобщены, то семейство из произведений a_i b_j с a_i из A и b_j из B линейно независимо над F.
LaTeX
$$$\mathrm{LinearIndependent}_F(\{a_i b_j\})$ for independent families a_i in A and b_j in B$$
Lean4
/-- If `A` and `L` are linearly disjoint, then for any `F`-linearly independent families
`{ u_i }`, `{ v_j }` of `A`, `L`, the products `{ u_i * v_j }`
are linearly independent over `F`. -/
theorem linearIndependent_mul' (H : A.LinearDisjoint L) {κ ι : Type*} {a : κ → A} {b : ι → L}
(ha : LinearIndependent F a) (hb : LinearIndependent F b) :
LinearIndependent F fun (i : κ × ι) ↦ (a i.1).1 * algebraMap L E (b i.2) := by
apply
Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat_left H ha <|
hb.map' _ (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toLinearEquiv.ker
