module module

`IndisputableMonolith.Astrophysics.CoronalLyapunovTime`

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 (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (8)

def referenceTime L41
def coronalTime L44
theorem coronalTime_pos L46
theorem coronalTime_succ_ratio L51
theorem coronalTime_strictly_increasing L55
theorem coronal_adjacent_ratio L65
structure CoronalLyapunovCert L70
def coronalLyapunovCert L77