no goals
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.586525
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
f : V →ₗ[K] V₁
h : Surjective ↑f
⊢ Module.rank K V = Module.rank K V₁ + Module.rank K { x // x ∈ LinearMap.ker f }
rw [← rank_range_add_rank_ker f, ← rank_range_of_surjective f h]