K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
⊢ Function.Injective ↑(dualMap f) → Function.Surjective ↑f
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
⊢ Function.Injective ↑(dualMap f) ↔ Function.Surjective ↑f
refine' ⟨_, fun h => dualMap_injective_of_surjective h⟩
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
⊢ ker (dualMap f) = ⊥ → range f = ⊤
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
⊢ Function.Injective ↑(dualMap f) → Function.Surjective ↑f
rw [← range_eq_top, ← ker_eq_bot]
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
h : ker (dualMap f) = ⊥
⊢ range f = ⊤
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
⊢ ker (dualMap f) = ⊥ → range f = ⊤
intro h
case h
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
h : ker (dualMap f) = ⊥
⊢ finrank K { x // x ∈ range f } = finrank K V₂
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
h : ker (dualMap f) = ⊥
⊢ range f = ⊤
apply FiniteDimensional.eq_top_of_finrank_eq
case h
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
h : finrank K { x // x ∈ ker (dualMap f) } = 0
⊢ finrank K { x // x ∈ range f } = finrank K V₂
case h
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
h : ker (dualMap f) = ⊥
⊢ finrank K { x // x ∈ range f } = finrank K V₂
rw [← finrank_eq_zero] at h
no goals
case h
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
h : finrank K { x // x ∈ ker (dualMap f) } = 0
⊢ finrank K { x // x ∈ range f } = finrank K V₂
rw [← add_zero (FiniteDimensional.finrank K <| LinearMap.range f), ← h, ←
  LinearMap.finrank_range_dualMap_eq_finrank_range, LinearMap.finrank_range_add_finrank_ker,
  Subspace.dual_finrank_eq]