of_basis_left — Mathlib

English

If a basis of A is also B-linearly independent, then A and B are linearly disjoint.

Русский

Если базис A одновременно линейно независим от B, то A и B линейно раздельны.

LaTeX

$$$\\text{Basis}_A\\text{ и }\\text{Basis}_B\\text{ так, что } (a_i)\\text{ линейно независимы над } B \\Rightarrow A \\perp_L B$$$

Lean4

/-- In a commutative ring, if a basis of `A` is also `B`-linearly independent,
then `A` and `B` are linearly disjoint. -/
theorem of_basis_left {ι : Type*} (a : Basis ι R A) (H : LinearIndependent B (A.val ∘ a)) : A.LinearDisjoint B :=
  of_basis_left_of_commute A B a H fun _ _ ↦ mul_comm _ _

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