∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (A : Matrix α β ℤ) [inst_2 : DecidableEq α],
  ↑(Finset.Icc
          (fun i =>
            ∑ j,
              ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ *
                -(A i j)⁻)
          fun i =>
          ∑ j,
            ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ *
              (A i j)⁺).card =
    ∏ i,
      ((fun i =>
              ∑ j,
                ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ *
                  (A i j)⁺)
            i -
          (fun i =>
              ∑ j,
                ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ *
                  -(A i j)⁻)
            i +
        1)