Connected algebras and their idempotents

An algebra is connected if its only central idempotents are 0 and 1. For a complete set of nonzero orthogonal idempotents f_i of a connected ring, any two indices are joined by a chain of nonzero corners f_i A f_j (eqvGen_corner): otherwise the sum of the f_l over the component of an index is a central idempotent other than 0 and 1.

def MultiplicativeBasisDeformations.IsConnectedRing (A : Type u_1) [Ring A] : Prop

A connected ring: the only central idempotents are 0 and 1.

theorem MultiplicativeBasisDeformations.eqvGen_corner {A : Type u_1} [Ring A] (hconn : IsConnectedRing A) {n : ℕ} {f : Fin n → A} (hf : CompleteOrthogonalIdempotents f) (hne : ∀ (i : Fin n), f i ≠ 0) (i j : Fin n) : Relation.EqvGen (fun (i j : Fin n) => ∃ (a : A), f i * a * f j ≠ 0) i j