K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
hinj : Injective ↑f
h : Module.rank K V = Module.rank K { x // x ∈ range f }
⊢ Surjective ↑f
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
hinj : Injective ↑f
⊢ Surjective ↑f
have h := rank_eq_of_injective _ hinj
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
hinj : Injective ↑f
h : finrank K V = finrank K { x // x ∈ range f }
⊢ Surjective ↑f
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
hinj : Injective ↑f
h : Module.rank K V = Module.rank K { x // x ∈ range f }
⊢ Surjective ↑f
rw [← finrank_eq_rank, ← finrank_eq_rank, natCast_inj] at h
no goals
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
hinj : Injective ↑f
h : finrank K V = finrank K { x // x ∈ range f }
⊢ Surjective ↑f
exact range_eq_top.1 (eq_top_of_finrank_eq h.symm)