Lean: f.d. algebra with only trivial idempotents is local, via Fitting on mulLeft

For a (noncommutative) finite-dimensional k-algebra A, apply Mathlib's LinearMap.eventually_isCompl_ker_pow_range_pow to LinearMap.mulLeft k a (rewrite with LinearMap.pow_mulLeft), combined with Filter.eventually_ge_atTop 1 so that n ≥ 1. Kernel and range of left multiplication by a^n are right ideals, so writing 1 = e + a^n*y (Submodule.mem_sup) makes e idempotent: e*e - e lies in ker (right ideal) and equals -(a^n*y*e) in range, and the two are disjoint. e = 1 gives a^n = 0; e = 0 gives a^n*y = 1, and injective_iff_surjective for mulLeft gives y*a^n = 1, so isUnit_pow_iff finishes. Then IsLocalRing.of_isUnit_or_isUnit_one_sub_self with IsNilpotent.isUnit_one_sub. This is the key step for 'Hom-finite idempotent complete categories are Krull-Schmidt'; induct on finrank (X ⟶ X), which drops for proper retracts.