module module

`IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk01`

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_010000 L17
theorem e_010001 L18
theorem e_010002 L19
theorem e_010003 L20
theorem e_010010 L21
theorem e_010011 L22
theorem e_010012 L23
theorem e_010013 L24
theorem e_010020 L25
theorem e_010021 L26
theorem e_010022 L27
theorem e_010023 L28
theorem e_010030 L29
theorem e_010031 L30
theorem e_010032 L31
theorem e_010033 L32
theorem e_010100 L33
theorem e_010101 L34
theorem e_010102 L35
theorem e_010103 L36
theorem e_010110 L37
theorem e_010111 L38
theorem e_010112 L39
theorem e_010113 L40
theorem e_010120 L41
theorem e_010121 L42
theorem e_010122 L43
theorem e_010123 L44
theorem e_010130 L45
theorem e_010131 L46
theorem e_010132 L47
theorem e_010133 L48
theorem e_010200 L49
theorem e_010201 L50
theorem e_010202 L51
theorem e_010203 L52
theorem e_010210 L53
theorem e_010211 L54
theorem e_010212 L55
theorem e_010213 L56
theorem e_010220 L57
theorem e_010221 L58
theorem e_010222 L59
theorem e_010223 L60
theorem e_010230 L61
theorem e_010231 L62
theorem e_010232 L63
theorem e_010233 L64
theorem e_010300 L65
theorem e_010301 L66
theorem e_010302 L67
theorem e_010303 L68
theorem e_010310 L69
theorem e_010311 L70
theorem e_010312 L71
theorem e_010313 L72
theorem e_010320 L73
theorem e_010321 L74
theorem e_010322 L75
theorem e_010323 L76
theorem e_010330 L77
theorem e_010331 L78
theorem e_010332 L79
theorem e_010333 L80
theorem e_011000 L81
theorem e_011001 L82
theorem e_011002 L83
theorem e_011003 L84
theorem e_011010 L85
theorem e_011011 L86
theorem e_011012 L87
theorem e_011013 L88
theorem e_011020 L89
theorem e_011021 L90
theorem e_011022 L91
theorem e_011023 L92
theorem e_011030 L93
theorem e_011031 L94
theorem e_011032 L95
theorem e_011033 L96

… and 176 more