theorem proved term proof

`phi_minimal_polynomial`

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

formal statement (Lean)

  87theorem phi_minimal_polynomial : phi ^ 2 - phi - 1 = 0 := by

Term-mode proof.

  88  have := phi_sq_eq
  89  linarith
  90

Lean names referenced from this declaration's body.