theorem mulRight_pow {k : Type u_1} [CommSemiring k] {R : Type u_2} [Ring R] [Algebra k R] (a : R) (n : ℕ) : LinearMap.mulRight k a ^ n = LinearMap.mulRight k (a ^ n)

The n-fold composition of right-multiplication by a equals right-multiplication by a ^ n, as a k-linear endomorphism of R.

theorem isLocalRing_of_finiteDimensional_of_no_nontrivial_idempotents (k : Type u_1) [Field k] (R : Type u_2) [Ring R] [Nontrivial R] [Algebra k R] [FiniteDimensional k R] (h_idem : ∀ (e : R), e * e = e → e = 0 ∨ e = 1) : IsLocalRing R

A finite-dimensional k-algebra R with no nontrivial idempotents is a local ring. The proof uses Fitting's lemma: for any a ∈ R, the operator mulRight a decomposes R as kernel and image of a sufficiently high power, producing an idempotent which by hypothesis is 0 or 1, hence either a is nilpotent (so 1 - a is a unit) or a is a unit.