rank

Mathlib.LinearAlgebra.Dimension.LinearMap

URI: https://scilib.ai/kg/mathlib#LinearMap.rank

← MathLib Explorer

English

For any linear map f: V → V', the rank of f is at most the rank of V'.

Русский

Для произвольного линейного отображения f: V → V' ранг f не превосходит ранга V'.

LaTeX

$$rank f ≤ Module.rank K V'$$

Lean4

/-- `rank f` is the rank of a `LinearMap` `f`, defined as the dimension of `f.range`. -/
abbrev rank (f : V →ₗ[K] V') : Cardinal :=
  Module.rank K (LinearMap.range f)

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

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

Разделы

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

Аффилиация

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