theorem
proved
hodge_implies_bsd
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Mathematics.HodgeConjectureStructure on GitHub at line 22.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
19theorem hodge_structure : hodge_from_ledger := bsd_structure
20
21/-- Hodge-structure scaffold implies BSD-side structural input. -/
22theorem hodge_implies_bsd (h : hodge_from_ledger) : bsd_from_ledger :=
23 h
24
25end HodgeConjectureStructure
26end Mathematics
27end IndisputableMonolith