of_basis_right — Mathlib

English

If { n_j } is an R-basis of N and ker(mulRightMap M n) = ⊥, then M and N are linearly disjoint.

Русский

Если { n_j } это R-базис N и ядро отображения ker(mulRightMap M n) = ⊥, тогда M и N линейно несовместны.

LaTeX

$$ker(\mathrm{mulRightMap}\,M\,n) = \bot \Rightarrow M \ LinearDisjoint\ N$$

Lean4

/-- If `{ n_i }` is an `R`-basis of `N`, which is also `M`-linearly independent,
then `M` and `N` are linearly disjoint. -/
theorem of_basis_right {ι : Type*} (n : Basis ι R N) (H : LinearMap.ker (mulRightMap M n) = ⊥) : M.LinearDisjoint N :=
  by
  -- need this instance otherwise `LinearMap.ker_eq_bot` does not work

  letI : AddCommGroup (ι →₀ M) := Finsupp.instAddCommGroup
  exact of_basis_right' M N n (LinearMap.ker_eq_bot.1 H)

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