noncomputable def BregmanMinc.N_i {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (σ τ : Equiv.Perm (Fin n)) (i : Fin n) : ℕ

$N_i(A, \sigma, \tau)$: number of columns $j$ such that $A_{ij} = 1$ and no earlier row in the $\tau$-ordering (i.e., $\tau^{-1}(m) < \tau^{-1}(i)$) has $\sigma(m) = j$. This counts the available choices at row $i$ in the Brégman-Minc proof.

theorem BregmanMinc.tree_identity (n : ℕ) (A : Matrix (Fin n) (Fin n) ℝ) (hA : ∀ (i j : Fin n), A i j = 0 ∨ A i j = 1) (τ : Equiv.Perm (Fin n)) (hP : 0 < {σ : Equiv.Perm (Fin n) | ∀ (i : Fin n), A i (σ i) = 1}.card) : ∑ σ : Equiv.Perm (Fin n) with ∀ (i : Fin n), A i (σ i) = 1, ∏ i : Fin n, 1 / ↑(N_i A σ τ i) = 1

Tree identity used in the proof of Brégman-Minc: for every row-ordering $\tau$, $\sum_\sigma \prod_i \frac{1}{N_i(A, \sigma, \tau)} = 1$, where the sum is over permutations $\sigma$ giving a perfect matching of the $0/1$ matrix $A$.