of_basis_right — Mathlib

English

If there exists an F-basis of B whose images are linearly independent over A, then A and B are linearly disjoint.

Русский

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

LaTeX

$$$\exists b \ : \text{Basis } ι F B, \; \mathrm{LinearIndependent}_A( B.\mathrm{val} \circ b ) \Rightarrow A \perp_F B$$$

Lean4

/-- If there exists an `F`-basis of `B` which remains linearly independent over `A`, then
`A` and `B` are linearly disjoint. -/
theorem of_basis_right {ι : Type*} (b : Basis ι F B) (H : LinearIndependent A (B.val ∘ b)) : A.LinearDisjoint B :=
  linearDisjoint_iff'.2 (.of_basis_right _ _ b H)

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