module module

`IndisputableMonolith.Mathematics.BirchTateStructure`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Mathematics.BirchSwinnertonDyerStructure module_import

declarations in this module (21)

structure K2RingOfIntegers L45
structure ZetaValue L50
def BirchTateConjecture L55
def IsTotallyReal L60
def w2Invariant L64
theorem birch_tate_for_Q L70
theorem birch_tate_quadratic L77
theorem lictenbaum_connection L83
theorem k2_phi_paths L94
theorem zeta_phi_orbits L103
theorem birch_tate_path_orbit_duality L110
theorem abelian_phi_product L117
theorem w2_phi_euler_characteristic L124
theorem has_bsd_structure L131
def birch_tate_from_ledger L133
theorem birch_tate_structure_chain L135
theorem birch_tate_implies_bsd L137
structure Resolution L143
theorem birch_tate_abelian_proven L152
theorem birch_tate_rs_prediction L159
theorem birch_tate_summary L167