eRank_one

Mathlib.LinearAlgebra.Matrix.Rank

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

← MathLib Explorer

English

The eRank of the 1-matrix equals the ENat-cardinality of the index set: eRank(1) = ENat.card m.

Русский

eRank(1) равен ENat.card m.

LaTeX

$$$\operatorname{eRank}(1) = \operatorname{ENat.card} \; m.$$$

Lean4

@[simp]
theorem eRank_one [Nontrivial R] [DecidableEq m] : (eRank (1 : Matrix m m R)) = ENat.card m := by
  rw [eRank, cRank_one, toENat_lift, ENat.card]

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

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

Разделы

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

Аффилиация

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