English
If { m_i } is a basis of M and { n_j } is a basis of N, and the family { m_i · n_j } is R-linearly independent, then M and N are linearly disjoint.
Русский
Если { m_i } является базисом M, а { n_j } базисом N, и семейство { m_i · n_j } линейно независимо над R, то M и N линейно несовместны.
LaTeX
$$LinearIndependent R (i : κ × ι) ↦ (m i.1).1 * (n i.2).1$$
Lean4
/-- If `{ m_i }` is an `R`-basis of `M`, if `{ n_j }` is an `R`-basis of `N`,
such that the family `{ m_i * n_j }` in `S` is `R`-linearly independent,
then `M` and `N` are linearly disjoint. -/
theorem of_basis_mul {κ ι : Type*} (m : Basis κ R M) (n : Basis ι R N)
(H : LinearIndependent R fun (i : κ × ι) ↦ (m i.1).1 * (n i.2).1) : M.LinearDisjoint N :=
by
rw [LinearIndependent] at H
exact of_basis_mul' M N m n H
