The Pure U(1) case with 1 fermion

We show that in this case the charge must be zero.

theorem PureU1.One.solEqZero (S : (PureU1 1).LinSols) : S = 0