of_subsingleton

Mathlib.LinearAlgebra.LinearIndependent.Defs

URI: https://scilib.ai/kg/mathlib#LinearIndepOn.of_subsingleton

English

If the base ring is a subsingleton, then LinearIndepOn R v s holds for any v and s.

Русский

Если кольцо базовое - одиночное, то LinearIndepOn R v s выполняется для любых v и s.

LaTeX

$$$\\\\text{[Subsingleton } R] \\\\Rightarrow \\\\mathrm{LinearIndepOn}_R v s.$$$

Lean4

@[nontriviality]
theorem of_subsingleton [Subsingleton R] : LinearIndepOn R v s :=
  linearIndependent_of_subsingleton

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru