`BookProof.NsLagrangianDet.phase_sum` {ι : Type*} (s : Finset ι) (w : ι → Fin 3 → ℝ) (a : Fin 3 → ℝ) : ∏ i ∈ s, phase (w i) a = phase (∑ i ∈ s, w i) a

Initializing...

`BookProof.NsLagrangianDet.phase_sum` {ι : Type*} (s : Finset ι) (w : ι → Fin 3 → ℝ) (a : Fin 3 → ℝ) : ∏ i ∈ s, phase (w i) a = phase (∑ i ∈ s, w i) a · Prove2Me