linearIndependent_right — Mathlib

English

If A and B are linearly disjoint, then any F-linearly independent family on A remains linearly independent over B.

Русский

Если A и B линейно разобщены, тогда любая F-линейно независимая семейство на A остаётся линейно независимой над B.

LaTeX

$$$A \perp_F B \Rightarrow \forall ι\, (b:\, ι \to A), \; \mathrm{LinearIndependent}_F(b) \Rightarrow \mathrm{LinearIndependent}_{A}(\mathrm{comp}(\mathrm{coe}_{A}, b)).$$$

Lean4

/-- If `A` and `B` are linearly disjoint, then any `F`-linearly independent family on `B` remains
linearly independent over `A`. -/
theorem linearIndependent_right (H : A.LinearDisjoint B) {ι : Type*} {b : ι → B} (hb : LinearIndependent F b) :
    LinearIndependent A (B.val ∘ b) :=
  (linearDisjoint_iff'.1 H).linearIndependent_right_of_flat hb

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