Linear subspaces cut out by idempotents

For a family e in a k-algebra, the (i,j) corner is the subspace e i * A * e j. We keep the range presentation because it exposes a literal ambient-algebra coordinate together with a witness.

def MagnitudeConjecture.idempotentCorner {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {ι : Type u_1} (e : ι → A) (i j : ι) : Submodule k A

The vector subspace e i * A * e j.

theorem MagnitudeConjecture.mem_idempotentCorner_iff {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {ι : Type u_1} (e : ι → A) (i j : ι) (x : A) : x ∈ idempotentCorner e i j ↔ ∃ (a : A), e i * a * e j = x