finrank_self

Mathlib.LinearAlgebra.Dimension.StrongRankCondition

URI: https://scilib.ai/kg/mathlib#Module.finrank_self

← MathLib Explorer

English

The finite rank of R as an R-module is the same as finrank_self, i.e., finrank_R(R) = 1 for a division ring or similar.

Русский

Финитный ранг R как R-модуля равен единице.

LaTeX

$$\\operatorname{finrank}_R(R) = 1$$

Lean4

/-- A ring satisfying `StrongRankCondition` (such as a `DivisionRing`) is one-dimensional as a
module over itself. -/
@[simp]
theorem finrank_self : finrank R R = 1 :=
  finrank_eq_of_rank_eq (by simp)

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

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

Разделы

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

Аффилиация

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