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
⊢ ker f = ⊥ ↔ range f = ⊤
rw [range_eq_top, ker_eq_bot, injective_iff_surjective]