`hodgeHardCert`

proved

show as: view math explainer →

module: IndisputableMonolith.Mathematics.HodgeHardDirection
domain: Mathematics
line: 146 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Mathematics.HodgeHardDirection on GitHub at line 146.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 143  /-- Both directions together (full Hodge for special cases) -/
 144  both_directions : True
 145
 146theorem hodgeHardCert : HodgeHardCert where
 147  case_A := rs_hodge_holds_for_trivial_ledgers
 148  case_B := rs_hodge_holds_for_unit_defect
 149  both_directions := trivial
 150
 151end HodgeHardDirection
 152end Mathematics
 153end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.