module module

`IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk03`

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

used by (1)

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

IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumAssemble module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert module_import

declarations in this module (256)

theorem e_030000 L17
theorem e_030001 L18
theorem e_030002 L19
theorem e_030003 L20
theorem e_030010 L21
theorem e_030011 L22
theorem e_030012 L23
theorem e_030013 L24
theorem e_030020 L25
theorem e_030021 L26
theorem e_030022 L27
theorem e_030023 L28
theorem e_030030 L29
theorem e_030031 L30
theorem e_030032 L31
theorem e_030033 L32
theorem e_030100 L33
theorem e_030101 L34
theorem e_030102 L35
theorem e_030103 L36
theorem e_030110 L37
theorem e_030111 L38
theorem e_030112 L39
theorem e_030113 L40
theorem e_030120 L41
theorem e_030121 L42
theorem e_030122 L43
theorem e_030123 L44
theorem e_030130 L45
theorem e_030131 L46
theorem e_030132 L47
theorem e_030133 L48
theorem e_030200 L49
theorem e_030201 L50
theorem e_030202 L51
theorem e_030203 L52
theorem e_030210 L53
theorem e_030211 L54
theorem e_030212 L55
theorem e_030213 L56
theorem e_030220 L57
theorem e_030221 L58
theorem e_030222 L59
theorem e_030223 L60
theorem e_030230 L61
theorem e_030231 L62
theorem e_030232 L63
theorem e_030233 L64
theorem e_030300 L65
theorem e_030301 L66
theorem e_030302 L67
theorem e_030303 L68
theorem e_030310 L69
theorem e_030311 L70
theorem e_030312 L71
theorem e_030313 L72
theorem e_030320 L73
theorem e_030321 L74
theorem e_030322 L75
theorem e_030323 L76
theorem e_030330 L77
theorem e_030331 L78
theorem e_030332 L79
theorem e_030333 L80
theorem e_031000 L81
theorem e_031001 L82
theorem e_031002 L83
theorem e_031003 L84
theorem e_031010 L85
theorem e_031011 L86
theorem e_031012 L87
theorem e_031013 L88
theorem e_031020 L89
theorem e_031021 L90
theorem e_031022 L91
theorem e_031023 L92
theorem e_031030 L93
theorem e_031031 L94
theorem e_031032 L95
theorem e_031033 L96

… and 176 more