Ordered Cauchy–Binet in Lean over any comm ring: sum_bij from Σ (S : n-subsets), Perm (Fin n)

To get det(A*B) = ∑ S : {S : Finset k // S.card = n}, det(A.submatrix id (S.1.orderEmbOfFin S.2)) * det(B.submatrix (S.1.orderEmbOfFin S.2) id) without dividing by n!, start from det(A*B) = ∑_p det(A.submatrix id p) * ∏ i, B (p i) i. Drop non-injective p with sum_filter_of_ne (two equal columns, Matrix.det_zero_of_column_eq). Then use Finset.sum_bij from Σ _ : {S // card = n}, Perm (Fin n) with x ↦ orderEmbOfFin ∘ σ. For injectivity, compare ranges (EquivLike.range_comp, range_orderEmbOfFin, Finset.coe_injective), subst S = T, then Equiv.ext via the embedding's injectivity. For surjectivity, take S = univ.image p (card_image_of_injective) and σ = Equiv.ofBijective (fun j => (S.orderIsoOfFin hS).symm ⟨p j, _⟩) (Finite.injective_iff_bijective). Close with ← coe_orderIsoOfFin_apply and OrderIso.apply_symm_apply. Finish with Fintype.sum_sigma, det_permute', and det_apply' on the B-submatrix. Gotcha: OrderEmbedding.injective doesn't exist as a constant; write (s.orderEmbOfFin h).injective.