module module

`IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk00`

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_000000 L17
theorem e_000001 L18
theorem e_000002 L19
theorem e_000003 L20
theorem e_000010 L21
theorem e_000011 L22
theorem e_000012 L23
theorem e_000013 L24
theorem e_000020 L25
theorem e_000021 L26
theorem e_000022 L27
theorem e_000023 L28
theorem e_000030 L29
theorem e_000031 L30
theorem e_000032 L31
theorem e_000033 L32
theorem e_000100 L33
theorem e_000101 L34
theorem e_000102 L35
theorem e_000103 L36
theorem e_000110 L37
theorem e_000111 L38
theorem e_000112 L39
theorem e_000113 L40
theorem e_000120 L41
theorem e_000121 L42
theorem e_000122 L43
theorem e_000123 L44
theorem e_000130 L45
theorem e_000131 L46
theorem e_000132 L47
theorem e_000133 L48
theorem e_000200 L49
theorem e_000201 L50
theorem e_000202 L51
theorem e_000203 L52
theorem e_000210 L53
theorem e_000211 L54
theorem e_000212 L55
theorem e_000213 L56
theorem e_000220 L57
theorem e_000221 L58
theorem e_000222 L59
theorem e_000223 L60
theorem e_000230 L61
theorem e_000231 L62
theorem e_000232 L63
theorem e_000233 L64
theorem e_000300 L65
theorem e_000301 L66
theorem e_000302 L67
theorem e_000303 L68
theorem e_000310 L69
theorem e_000311 L70
theorem e_000312 L71
theorem e_000313 L72
theorem e_000320 L73
theorem e_000321 L74
theorem e_000322 L75
theorem e_000323 L76
theorem e_000330 L77
theorem e_000331 L78
theorem e_000332 L79
theorem e_000333 L80
theorem e_001000 L81
theorem e_001001 L82
theorem e_001002 L83
theorem e_001003 L84
theorem e_001010 L85
theorem e_001011 L86
theorem e_001012 L87
theorem e_001013 L88
theorem e_001020 L89
theorem e_001021 L90
theorem e_001022 L91
theorem e_001023 L92
theorem e_001030 L93
theorem e_001031 L94
theorem e_001032 L95
theorem e_001033 L96

… and 176 more