cRank_subsingleton

Mathlib.LinearAlgebra.Matrix.Rank

URI: https://scilib.ai/kg/mathlib#Matrix.cRank_subsingleton

English

If the base ring R is a Subsingleton, then for any matrix A, its cRank equals 1.

Русский

Если кольцо R состоит из одного элемента (subsingleton), то для любой матрицы A cRank = 1.

LaTeX

$$$\text{If } [\text{Subsingleton } R],\ \ A.ctRank = 1.$$$

Lean4

@[simp]
theorem cRank_subsingleton [Subsingleton R] (A : Matrix m n R) : A.cRank = 1 :=
  rank_subsingleton _ _

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

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

Разделы

Аффилиация

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