module module

`IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk13`

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_310000 L17
theorem e_310001 L18
theorem e_310002 L19
theorem e_310003 L20
theorem e_310010 L21
theorem e_310011 L22
theorem e_310012 L23
theorem e_310013 L24
theorem e_310020 L25
theorem e_310021 L26
theorem e_310022 L27
theorem e_310023 L28
theorem e_310030 L29
theorem e_310031 L30
theorem e_310032 L31
theorem e_310033 L32
theorem e_310100 L33
theorem e_310101 L34
theorem e_310102 L35
theorem e_310103 L36
theorem e_310110 L37
theorem e_310111 L38
theorem e_310112 L39
theorem e_310113 L40
theorem e_310120 L41
theorem e_310121 L42
theorem e_310122 L43
theorem e_310123 L44
theorem e_310130 L45
theorem e_310131 L46
theorem e_310132 L47
theorem e_310133 L48
theorem e_310200 L49
theorem e_310201 L50
theorem e_310202 L51
theorem e_310203 L52
theorem e_310210 L53
theorem e_310211 L54
theorem e_310212 L55
theorem e_310213 L56
theorem e_310220 L57
theorem e_310221 L58
theorem e_310222 L59
theorem e_310223 L60
theorem e_310230 L61
theorem e_310231 L62
theorem e_310232 L63
theorem e_310233 L64
theorem e_310300 L65
theorem e_310301 L66
theorem e_310302 L67
theorem e_310303 L68
theorem e_310310 L69
theorem e_310311 L70
theorem e_310312 L71
theorem e_310313 L72
theorem e_310320 L73
theorem e_310321 L74
theorem e_310322 L75
theorem e_310323 L76
theorem e_310330 L77
theorem e_310331 L78
theorem e_310332 L79
theorem e_310333 L80
theorem e_311000 L81
theorem e_311001 L82
theorem e_311002 L83
theorem e_311003 L84
theorem e_311010 L85
theorem e_311011 L86
theorem e_311012 L87
theorem e_311013 L88
theorem e_311020 L89
theorem e_311021 L90
theorem e_311022 L91
theorem e_311023 L92
theorem e_311030 L93
theorem e_311031 L94
theorem e_311032 L95
theorem e_311033 L96

… and 176 more