Proof of `Full response obstructions are effective profiles plus selected atoms` (5th statement)
groundedproofs/Lax342547Proofs/EffectiveObstructions.lean · lax-342547
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Choose linear retractions onto both factor spaces. Their images of coordinate basis vectors lie in the two factors. The row and column conditions reconstruct the matrix as a finite sum of those outer products.