theorem proved term proof

`hodge_implies_bsd`

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

formal statement (Lean)

  22theorem hodge_implies_bsd (h : hodge_from_ledger) : bsd_from_ledger :=

Term-mode proof.

  23  h
  24
  25end HodgeConjectureStructure
  26end Mathematics
  27end IndisputableMonolith

Lean names referenced from this declaration's body.

bsd_from_ledger in IndisputableMonolith.Mathematics.BirchSwinnertonDyerStructure decl_use
hodge_from_ledger in IndisputableMonolith.Mathematics.HodgeConjectureStructure decl_use