of_basis_right — Mathlib

English

If A ⊔ B = S and a basis of A is given, the corresponding left-basis for B yields a basis of S when mapped to B.

Русский

Если A ⊔ B = S и дан базис A, соответствующий левый базис для B даёт базис S после отображения в B.

LaTeX

$$$H.basisOfBasisLeft H' b i = algebraMap A S (b i)$$$

Lean4

/-- If a basis of `B` is also `A`-linearly independent, then `A` and `B` are linearly disjoint. -/
theorem of_basis_right {ι : Type*} (b : Basis ι R B) (H : LinearIndependent A (B.val ∘ b)) : A.LinearDisjoint B :=
  by
  rw [← mulRightMap_ker_eq_bot_iff_linearIndependent] at H
  exact Submodule.LinearDisjoint.of_basis_right _ _ b H

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