rank_one

Mathlib.LinearAlgebra.Matrix.Rank

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

← MathLib Explorer

English

The rank of the identity matrix I_n is n, i.e., rank(I_n) = |n|.

Русский

Ранг матрицы единиц I_n равен n, то есть rank(I_n) = |n|.

LaTeX

$$$\operatorname{rank}(I_n) = |n|$.$$

Lean4

@[simp]
theorem rank_one [Nontrivial R] [DecidableEq n] : rank (1 : Matrix n n R) = Fintype.card n := by
  rw [rank, mulVecLin_one, LinearMap.range_id, finrank_top, finrank_pi]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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