of_basis_left' — Mathlib

English

If m is a basis of M and the induced mulLeftMap N m is injective, then M and N are linearly disjoint.

Русский

Если m — базис пространства M и mulLeftMap N m инъективен, то M и N линейно несовместны.

LaTeX

$$M.LinearDisjoint N$$

Lean4

/-- If `{ m_i }` is an `R`-basis of `M`, which is also `N`-linearly independent
(in this result it is stated as `Submodule.mulLeftMap` is injective),
then `M` and `N` are linearly disjoint. -/
theorem of_basis_left' {ι : Type*} (m : Basis ι R M) (H : Function.Injective (mulLeftMap N m)) : M.LinearDisjoint N :=
  by
  classical
    simp_rw [mulLeftMap_eq_mulMap_comp, ← Basis.coe_repr_symm, ← LinearEquiv.coe_rTensor, LinearEquiv.comp_coe,
    LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.injective_comp] at H
  exact ⟨H⟩

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