Hopf problem: toric · toric space 2

Supporting definitions and proofs for this stage of the six-sphere construction.

theorem Mathoverflow1973.ToricCharts.equal_columns_of_left_inverse {A B : Matrix (Fin 3) (Fin 3) ℤ} (hBA : B * A = 1) {j k : Fin 3} (hcol : ∀ (i : Fin 3), A i j = A i k) : j = k