Proof of `Stabilized ranks and the radical quotient` (3rd statement)
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
The restricted pairing factors through the image of the subspace in the radical quotient. Equality of ranks forces that image to fill the quotient.