rank_le_range

Mathlib.LinearAlgebra.Dimension.LinearMap

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

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

theorem rank_le_range (f : V →ₗ[K] V') : rank f ≤ Module.rank K V' :=
  Submodule.rank_le _

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

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

Разделы

Аффилиация

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