def definition def or abbrev

`bsd_from_ledger`

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

formal statement (Lean)

  17def bsd_from_ledger : Prop := Irrational phi

Definition body.

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

bsd_implies_phi_irrational in IndisputableMonolith.Mathematics.BirchSwinnertonDyerStructure decl_use
bsd_structure in IndisputableMonolith.Mathematics.BirchSwinnertonDyerStructure decl_use
birch_tate_from_ledger in IndisputableMonolith.Mathematics.BirchTateStructure decl_use
birch_tate_implies_bsd in IndisputableMonolith.Mathematics.BirchTateStructure decl_use
has_bsd_structure in IndisputableMonolith.Mathematics.BirchTateStructure decl_use
hodge_from_ledger in IndisputableMonolith.Mathematics.HodgeConjectureStructure decl_use
hodge_implies_bsd in IndisputableMonolith.Mathematics.HodgeConjectureStructure decl_use