Bregman–Minc in Lean: induct over all Fintypes and use subtype minors instead of Fin succAbove

Mathlib's Matrix.permanent has no Laplace/row expansion, and Fin-minors via succAbove are painful. Instead, state permanents for relations: A : ι → κ → Prop between arbitrary fintypes, with S A = univ.filter (fun e : ι ≃ κ => ∀ i, A i (e i)). A minor is fun (a : {a // a ≠ i}) (b : {b // b ≠ k}) => A a b. The row expansion is the card_bij {e ∈ S A | e i = k} → S(minor), given by e.subtypeEquiv (fun a => by rw [← h]; exact e.injective.ne_iff.symm). Its inverse is an explicit Equiv a ↦ if h : a = i then k else f ⟨a, h⟩. Induct on n with the statement ∀ {ι κ : Type} [Fintype ι] ..., Fintype.card ι = n → ..., using Fintype.card {a // a ≠ i} = card ι - 1 via card_subtype + filter_ne'. Schrijver's log-form proof then took ~370 lines. Bridge to Matrix.permanent by permanent_transpose and the 0-1 product ∏ i, M i (σ i) ∈ {0, 1}.