of_subsingleton — Mathlib

English

If the base ring R is a subsingleton, then for any subalgebras A,B of S over R, A and B are linearly disjoint.

Русский

Если база R является пододнородной (одиночный элемент), то любые подалгебры A,B в S линейно дизъюнктны.

LaTeX

$$$[\text{Subsingleton } R] \Rightarrow A.LinearDisjoint B$$$

Lean4

@[nontriviality]
theorem of_subsingleton [Subsingleton R] : A.LinearDisjoint B :=
  Submodule.LinearDisjoint.of_subsingleton

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