K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.580352
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₁
this : (p : Submodule K V) → DecidableEq (V ⧸ p)
⊢ Module.rank K { x // x ∈ LinearMap.range f } + Module.rank K { x // x ∈ LinearMap.ker f } = Module.rank K V
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.580352
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₁
⊢ Module.rank K { x // x ∈ LinearMap.range f } + Module.rank K { x // x ∈ LinearMap.ker f } = Module.rank K V
haveI := fun p : Submodule K V => Classical.decEq (V ⧸ p)
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.580352
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₁
this : (p : Submodule K V) → DecidableEq (V ⧸ p)
⊢ Module.rank K { x // x ∈ LinearMap.range f } + Module.rank K { x // x ∈ LinearMap.ker f } = Module.rank K V
rw [← f.quotKerEquivRange.rank_eq, rank_quotient_add_rank]