Binet_Cauchy_Identity
Provedalgebraidentitiesproofwiki
The Binet-Cauchy identity: (sum a_i c_i)(sum b_j d_j) = sum_{i<j} (a_i b_j - a_j b_i)(c_i d_j - c_j d_i) + (sum a_i d_i)(sum b_j c_j).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Binet_Cauchy_Identity (n : ℕ) (a b c d : Fin n → ℝ) : (∑ i, a i * c i) * (∑ j, b j * d j) - (∑ i, a i * d i) * (∑ j, b j * c j) = ∑ i, ∑ j, (a i * b j - a j * b i) * (c i * d j - c j * d i) / 2 := by sorry
Source