linearIndependent_mul — Mathlib

English

Analogous relation for the left basis; the left basis representation matches the corresponding algebra map when evaluating at an element.

Русский

Аналогичное соотношение для левого базиса; представление левого базиса совпадает с соответствующим алгебраическим отображением при вычислении на элементе.

LaTeX

$$$\text{basisOfBasisLeft_repr_apply}(...)$$$

Lean4

/-- If `A` and `B` are linearly disjoint, then for any `F`-linearly independent families
`{ u_i }`, `{ v_j }` of `A`, `B`, the products `{ u_i * v_j }`
are linearly independent over `F`. -/
theorem linearIndependent_mul (H : A.LinearDisjoint B) {κ ι : Type*} {a : κ → A} {b : ι → B}
    (ha : LinearIndependent F a) (hb : LinearIndependent F b) :
    LinearIndependent F fun (i : κ × ι) ↦ (a i.1).1 * (b i.2).1 :=
  (linearDisjoint_iff'.1 H).linearIndependent_mul_of_flat_left ha hb

Похожие утверждения