linearIndependent_of_subsingleton

English

If the base ring is a subsingleton, any family is linearly independent.

Русский

Если множество элементов кольца состоит из одного элемента, любое семейство линейно независимо.

LaTeX

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

Lean4

@[nontriviality]
theorem linearIndependent_of_subsingleton [Subsingleton R] : LinearIndependent R v :=
  linearIndependent_iffₛ.2 fun _l _l' _hl => Subsingleton.elim _ _

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