Hopf problem: recognition · smale 13 #
Supporting definitions and proofs for this stage of the six-sphere construction.
theorem
Mathoverflow1973.Smale.HomologyTransport.matrix_sizes_eq_of_bijective
{R : Type u_1}
[CommRing R]
[StrongRankCondition R]
{r c : ℕ}
(A : Matrix (Fin r) (Fin c) R)
(hA : Function.Bijective A.mulVec)
: