of_basis_mul — Mathlib

English

If A is linearly disjoint from B, then any F-independent family on B remains L-independent after embedding into E.

Русский

Если A линейно разобщено с B, любая F‑независимая семейство на B остается L‑независимой после включения в E.

LaTeX

$$$A \perp_F B \Rightarrow \text{LinearIndependent}_F(b) \Rightarrow \text{LinearIndependent}_A(\text{coefficients}(b))$$$

Lean4

/-- If there are `F`-bases `{ u_i }`, `{ v_j }` of `A`, `B`, such that the products
`{ u_i * v_j }` are linearly independent over `F`, then `A` and `B` are linearly disjoint. -/
theorem of_basis_mul {κ ι : Type*} (a : Basis κ F A) (b : Basis ι F B)
    (H : LinearIndependent F fun (i : κ × ι) ↦ (a i.1).1 * (b i.2).1) : A.LinearDisjoint B :=
  linearDisjoint_iff'.2 (.of_basis_mul _ _ a b H)

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