pith. machine review for the scientific record. sign in
theorem proved term proof

hpOperator_eigenvector_pos

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  68theorem hpOperator_eigenvector_pos (q : ℕ) (a : ℤ) :
  69    (hpOperator q a).mulVec ![1, 1] = frobeniusAngle q a • ![1, 1] := by

proof body

Term-mode proof.

  70  ext i
  71  fin_cases i <;>
  72    simp [hpOperator, Matrix.mulVec, Matrix.cons_val', Matrix.empty_val',
  73          Matrix.cons_val_fin_one, Matrix.cons_val_zero, Matrix.cons_val_one,
  74          Matrix.head_cons, Matrix.head_fin_const,
  75          Matrix.cons_dotProduct, Matrix.dotProduct_empty, Fin.sum_univ_two] <;>
  76    ring
  77
  78/-- The vector `(1, -1)` is an eigenvector with eigenvalue `-θ`. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.