module module

`IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk10`

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_220000 L17
theorem e_220001 L18
theorem e_220002 L19
theorem e_220003 L20
theorem e_220010 L21
theorem e_220011 L22
theorem e_220012 L23
theorem e_220013 L24
theorem e_220020 L25
theorem e_220021 L26
theorem e_220022 L27
theorem e_220023 L28
theorem e_220030 L29
theorem e_220031 L30
theorem e_220032 L31
theorem e_220033 L32
theorem e_220100 L33
theorem e_220101 L34
theorem e_220102 L35
theorem e_220103 L36
theorem e_220110 L37
theorem e_220111 L38
theorem e_220112 L39
theorem e_220113 L40
theorem e_220120 L41
theorem e_220121 L42
theorem e_220122 L43
theorem e_220123 L44
theorem e_220130 L45
theorem e_220131 L46
theorem e_220132 L47
theorem e_220133 L48
theorem e_220200 L49
theorem e_220201 L50
theorem e_220202 L51
theorem e_220203 L52
theorem e_220210 L53
theorem e_220211 L54
theorem e_220212 L55
theorem e_220213 L56
theorem e_220220 L57
theorem e_220221 L58
theorem e_220222 L59
theorem e_220223 L60
theorem e_220230 L61
theorem e_220231 L62
theorem e_220232 L63
theorem e_220233 L64
theorem e_220300 L65
theorem e_220301 L66
theorem e_220302 L67
theorem e_220303 L68
theorem e_220310 L69
theorem e_220311 L70
theorem e_220312 L71
theorem e_220313 L72
theorem e_220320 L73
theorem e_220321 L74
theorem e_220322 L75
theorem e_220323 L76
theorem e_220330 L77
theorem e_220331 L78
theorem e_220332 L79
theorem e_220333 L80
theorem e_221000 L81
theorem e_221001 L82
theorem e_221002 L83
theorem e_221003 L84
theorem e_221010 L85
theorem e_221011 L86
theorem e_221012 L87
theorem e_221013 L88
theorem e_221020 L89
theorem e_221021 L90
theorem e_221022 L91
theorem e_221023 L92
theorem e_221030 L93
theorem e_221031 L94
theorem e_221032 L95
theorem e_221033 L96

… and 176 more