# The rank of a linear map #

## Main Definition #

• LinearMap.rank: The rank of a linear map.
@[reducible, inline]
abbrev LinearMap.rank {K : Type u} {V : Type v} {V' : Type v'} [Ring K] [] [Module K V] [] [Module K V'] (f : V →ₗ[K] V') :

rank f is the rank of a LinearMap f, defined as the dimension of f.range.

Equations
• f.rank =
Instances For
theorem LinearMap.rank_le_range {K : Type u} {V : Type v} {V' : Type v'} [Ring K] [] [Module K V] [] [Module K V'] (f : V →ₗ[K] V') :
f.rank Module.rank K V'
theorem LinearMap.rank_le_domain {K : Type u} {V : Type v} {V₁ : Type v} [Ring K] [] [Module K V] [] [Module K V₁] (f : V →ₗ[K] V₁) :
f.rank
@[simp]
theorem LinearMap.rank_zero {K : Type u} {V : Type v} {V' : Type v'} [Ring K] [] [Module K V] [] [Module K V'] [] :
theorem LinearMap.rank_comp_le_left {K : Type u} {V : Type v} {V' : Type v'} {V'' : Type v''} [Ring K] [] [Module K V] [] [Module K V'] [AddCommGroup V''] [Module K V''] (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') :
(f ∘ₗ g).rank f.rank
theorem LinearMap.lift_rank_comp_le_right {K : Type u} {V : Type v} {V' : Type v'} {V'' : Type v''} [Ring K] [] [Module K V] [] [Module K V'] [AddCommGroup V''] [Module K V''] (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') :
theorem LinearMap.lift_rank_comp_le {K : Type u} {V : Type v} {V' : Type v'} {V'' : Type v''} [Ring K] [] [Module K V] [] [Module K V'] [AddCommGroup V''] [Module K V''] (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') :

The rank of the composition of two maps is less than the minimum of their ranks.

theorem LinearMap.rank_comp_le_right {K : Type u} {V : Type v} {V' : Type v'} {V'₁ : Type v'} [Ring K] [] [Module K V] [] [Module K V'] [AddCommGroup V'₁] [Module K V'₁] (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) :
(f ∘ₗ g).rank g.rank
theorem LinearMap.rank_comp_le {K : Type u} {V : Type v} {V' : Type v'} {V'₁ : Type v'} [Ring K] [] [Module K V] [] [Module K V'] [AddCommGroup V'₁] [Module K V'₁] (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) :
(f ∘ₗ g).rank min f.rank g.rank

The rank of the composition of two maps is less than the minimum of their ranks.

See lift_rank_comp_le for the universe-polymorphic version.

theorem LinearMap.rank_add_le {K : Type u} {V : Type v} {V' : Type v'} [] [] [Module K V] [] [Module K V'] (f : V →ₗ[K] V') (g : V →ₗ[K] V') :
(f + g).rank f.rank + g.rank
theorem LinearMap.rank_finset_sum_le {K : Type u} {V : Type v} {V' : Type v'} [] [] [Module K V] [] [Module K V'] {η : Type u_1} (s : ) (f : ηV →ₗ[K] V') :
(ds, f d).rank ds, (f d).rank
theorem LinearMap.le_rank_iff_exists_linearIndependent {K : Type u} {V : Type v} {V' : Type v'} [] [] [Module K V] [] [Module K V'] {c : Cardinal.{v'}} {f : V →ₗ[K] V'} :
c f.rank ∃ (s : Set V), = LinearIndependent K fun (x : s) => f x
theorem LinearMap.le_rank_iff_exists_linearIndependent_finset {K : Type u} {V : Type v} {V' : Type v'} [] [] [Module K V] [] [Module K V'] {n : } {f : V →ₗ[K] V'} :
n f.rank ∃ (s : ), s.card = n LinearIndependent K fun (x : s) => f x