module module

`IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk15`

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_330000 L17
theorem e_330001 L18
theorem e_330002 L19
theorem e_330003 L20
theorem e_330010 L21
theorem e_330011 L22
theorem e_330012 L23
theorem e_330013 L24
theorem e_330020 L25
theorem e_330021 L26
theorem e_330022 L27
theorem e_330023 L28
theorem e_330030 L29
theorem e_330031 L30
theorem e_330032 L31
theorem e_330033 L32
theorem e_330100 L33
theorem e_330101 L34
theorem e_330102 L35
theorem e_330103 L36
theorem e_330110 L37
theorem e_330111 L38
theorem e_330112 L39
theorem e_330113 L40
theorem e_330120 L41
theorem e_330121 L42
theorem e_330122 L43
theorem e_330123 L44
theorem e_330130 L45
theorem e_330131 L46
theorem e_330132 L47
theorem e_330133 L48
theorem e_330200 L49
theorem e_330201 L50
theorem e_330202 L51
theorem e_330203 L52
theorem e_330210 L53
theorem e_330211 L54
theorem e_330212 L55
theorem e_330213 L56
theorem e_330220 L57
theorem e_330221 L58
theorem e_330222 L59
theorem e_330223 L60
theorem e_330230 L61
theorem e_330231 L62
theorem e_330232 L63
theorem e_330233 L64
theorem e_330300 L65
theorem e_330301 L66
theorem e_330302 L67
theorem e_330303 L68
theorem e_330310 L69
theorem e_330311 L70
theorem e_330312 L71
theorem e_330313 L72
theorem e_330320 L73
theorem e_330321 L74
theorem e_330322 L75
theorem e_330323 L76
theorem e_330330 L77
theorem e_330331 L78
theorem e_330332 L79
theorem e_330333 L80
theorem e_331000 L81
theorem e_331001 L82
theorem e_331002 L83
theorem e_331003 L84
theorem e_331010 L85
theorem e_331011 L86
theorem e_331012 L87
theorem e_331013 L88
theorem e_331020 L89
theorem e_331021 L90
theorem e_331022 L91
theorem e_331023 L92
theorem e_331030 L93
theorem e_331031 L94
theorem e_331032 L95
theorem e_331033 L96

… and 176 more