of_subsingleton — Mathlib

English

If the base ring R is a singleton (subsingleton), then for any submodules M,N of S, the pair M,N are automatically linearly disjoint over R.

Русский

Если база R сводится к одному элементу, то для любых подмодулей M,N в S пара M,N автоматически линейно несовместна над R.

LaTeX

$$$[Subsingleton\,R] \Rightarrow M \mathrm{LinearDisjoint} N$$$

Lean4

@[nontriviality]
theorem of_subsingleton [Subsingleton R] : M.LinearDisjoint N :=
  haveI : Subsingleton S := Module.subsingleton R S
  ⟨Function.injective_of_subsingleton _⟩

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