theorem proved term proof

`Q3_max_eigenvalue_eq`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  56theorem Q3_max_eigenvalue_eq : Q3_max_eigenvalue = 2 * Q3_degree := by

Term-mode proof.

  57  unfold Q3_max_eigenvalue Q3_degree; omega
  58
  59/-- The multiplicities are {1, 3, 3, 1} = binomial coefficients C(3,k). -/

Lean names referenced from this declaration's body.