theorem DimensionFormula.dimension_formula {F : Type u_1} [DivisionRing F] {V : Type u_2} [AddCommGroup V] [Module F V] [FiniteDimensional F V] {W : Type u_3} [AddCommGroup W] [Module F W] (T : V →ₗ[F] W) : Module.finrank F ↥T.ker + Module.finrank F ↥T.range = Module.finrank F V