rank_le_domain

Mathlib.LinearAlgebra.Dimension.LinearMap

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

English

The rank of the composition f ∘ g is at most the rank of f on the left.

Русский

Ранг композиции f ∘ g не превышает ранг f слева.

LaTeX

$$rank (f ∘ g) ≤ rank f$$

Lean4

theorem rank_le_domain (f : V →ₗ[K] V₁) : rank f ≤ Module.rank K V :=
  rank_range_le _

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

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

Разделы

Аффилиация

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