`BookProof.SmHiggsVacuum.gaugeMassForm_smul` (X : Fin 3 → Matrix (Fin 4) (Fin 4) ℝ) (u : Fin 4 → ℝ) (c : ℝ) : gaugeMassForm (fun i => c • X i) u = c ^ 2 * gaugeMassForm X u

Initializing...

`BookProof.SmHiggsVacuum.gaugeMassForm_smul` (X : Fin 3 → Matrix (Fin 4) (Fin 4) ℝ) (u : Fin 4 → ℝ) (c : ℝ) : gaugeMassForm (fun i => c • X i) u = c ^ 2 * gaugeMassForm X u · Prove2Me