of_basis_left — Mathlib

English

If {m_i} is an R-basis of M and ker(mulLeftMap N m) = ⊥, then M and N are linearly disjoint.

Русский

Если множество элементов {m_i} является R-базисом подмодуля M, и ядро отображения ker(mulLeftMap N m) = ⊥, то M и N линейно несовместны.

LaTeX

$$ker(\mathrm{mulLeftMap}\,N\,m) = \bot \Rightarrow M \ LinearDisjoint\ N$$

Lean4

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

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

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