def definition def or abbrev

`birch_tate_from_ledger`

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

formal statement (Lean)

 133def birch_tate_from_ledger : Prop := bsd_from_ledger

Definition body.

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

birch_tate_implies_bsd in IndisputableMonolith.Mathematics.BirchTateStructure decl_use
birch_tate_structure_chain in IndisputableMonolith.Mathematics.BirchTateStructure decl_use

Lean names referenced from this declaration's body.

bsd_from_ledger in IndisputableMonolith.Mathematics.BirchSwinnertonDyerStructure decl_use