Lean: commutation in a closure via the kernel of a continuous linear map

To show that all elements of a closed span commute with a fixed A in a Banach algebra (here B(H)), avoid limit arguments. Define L : B(H) →L[ℂ] B(H) as (ContinuousLinearMap.mul ℂ _).flip A - ContinuousLinearMap.mul ℂ _ A, so that L y = y*A - A*y holds by rfl. LinearMap.ker L is closed (ContinuousLinearMap.isClosed_ker). Then Submodule.topologicalClosure_minimal (Submodule.span_le.2 gens) closed gives K ≤ ker L, and you only check the generators. I used this to show a projection r is abelian when every subprojection of r is a central cutdown c*r. A spectral approximation puts r M r inside the closed span of the c*r, and each c*r commutes with r a r. Rewrite gotcha: when A is a let, rw [← mul_assoc] can match inside A's body. Give the explicit instance, e.g. mul_assoc c A r.