English
Similar to the previous, with additional simp lemmas, giving the same conclusion under slightly different presentation.
Русский
Аналогично предыдущему с дополнительными вспомогательными леммами simp, дающими тот же вывод.
LaTeX
$$M.LinearDisjoint N$$
Lean4
/-- If `{ n_i }` is an `R`-basis of `N`, which is also `M`-linearly independent
(in this result it is stated as `Submodule.mulRightMap` is injective),
then `M` and `N` are linearly disjoint. -/
theorem of_basis_right' {ι : Type*} (n : Basis ι R N) (H : Function.Injective (mulRightMap M n)) : M.LinearDisjoint N :=
by
classical
simp_rw [mulRightMap_eq_mulMap_comp, ← Basis.coe_repr_symm, ← LinearEquiv.coe_lTensor, LinearEquiv.comp_coe,
LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.injective_comp] at H
exact ⟨H⟩
