Proofs.Mat ↔ Mathlib Matrix bridge #

The proof suite works over Mat m n := Fin m → Fin n → ℝ (Tensor.lean), which is definitionally Mathlib's Matrix (Fin m) (Fin n) ℝ. The suite defines its own mulVec / outer / mul / transpose on that function type rather than reusing Mathlib's. The four lemmas here reconcile the operation names, so a downstream consumer can apply Mathlib's matrix-algebra API (mul_assoc, transpose_transpose, mulVec_mulVec, …) to the suite's outputs without re-deriving the correspondence by hand.

Opt-in by design: the core suite does not import this file, so Tensor.lean's import surface — and every build that doesn't need Mathlib's Matrix — stays exactly as it was. Import LeanMlir.Proofs.Codegen.MatBridge only when you want the interop.

Matrix.of is the identity equiv (Fin m → Fin n → ℝ) ≃ Matrix …; it carries no data (Matrix.of A is defeq to A) but lets instance resolution see the value as a Matrix, so Mathlib's *ᵥ / ᵀ / * notation applies.