English
If b is a linearly independent family over R and c is linearly independent over S, then the family {b_i • c_j} is linearly independent over R.
Русский
Если {b_i} линейно независима над R и {c_j} линейно независима над S, то {b_i • c_j} линейно независима над R.
LaTeX
$$$$ LinearIndependent_R b \\rightarrow LinearIndependent_S c \\rightarrow LinearIndependent_R (\\lambda p: \\iota \\times \\iota' , b p.1 • c p.2) $$$$
Lean4
theorem linearIndependent_smul {ι : Type*} {b : ι → S} {ι' : Type*} {c : ι' → A} (hb : LinearIndependent R b)
(hc : LinearIndependent S c) : LinearIndependent R fun p : ι × ι' ↦ b p.1 • c p.2 := by
classical
rw [← linearIndependent_equiv' (.prodComm ..) (g := fun p : ι' × ι ↦ b p.2 • c p.1) rfl, LinearIndependent,
linearCombination_smul]
simpa using Function.Injective.comp hc ((mapRange_injective _ (map_zero _) hb).comp <| Equiv.injective _)
