instNonemptyTransvectionStructOfNontrivial

English

If the index set n is nontrivial, there exists a TransvectionStruct n R, i.e., a transvection data structure on n over R.

Русский

Если множество индексов n ненулевое, существует структура трансваекции на n над кольцом R.

LaTeX

$$$\\text{If }\\operatorname{Nontrivial}(n)\\text{, then }\\exists t:\\text{TransvectionStruct }n\\,R\\,.$$$

Lean4

instance [Nontrivial n] : Nonempty (TransvectionStruct n R) :=
  by
  choose x y hxy using exists_pair_ne n
  exact ⟨⟨x, y, hxy, 0⟩⟩

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