rwa [Function.Bijective.sum_comp hp (fun j ↦ a (p i) j * x j)]
x : Fin 3 → ℝ
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
he : propEqs x a
i : Fin 3
hi : ∑ j : Fin 3, a (p i) j * x j = 0
⊢ ∑ j : Fin 3, a (p i) (p j) * x (p j) = 0
no goals