module module

`IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk02`

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_020000 L17
theorem e_020001 L18
theorem e_020002 L19
theorem e_020003 L20
theorem e_020010 L21
theorem e_020011 L22
theorem e_020012 L23
theorem e_020013 L24
theorem e_020020 L25
theorem e_020021 L26
theorem e_020022 L27
theorem e_020023 L28
theorem e_020030 L29
theorem e_020031 L30
theorem e_020032 L31
theorem e_020033 L32
theorem e_020100 L33
theorem e_020101 L34
theorem e_020102 L35
theorem e_020103 L36
theorem e_020110 L37
theorem e_020111 L38
theorem e_020112 L39
theorem e_020113 L40
theorem e_020120 L41
theorem e_020121 L42
theorem e_020122 L43
theorem e_020123 L44
theorem e_020130 L45
theorem e_020131 L46
theorem e_020132 L47
theorem e_020133 L48
theorem e_020200 L49
theorem e_020201 L50
theorem e_020202 L51
theorem e_020203 L52
theorem e_020210 L53
theorem e_020211 L54
theorem e_020212 L55
theorem e_020213 L56
theorem e_020220 L57
theorem e_020221 L58
theorem e_020222 L59
theorem e_020223 L60
theorem e_020230 L61
theorem e_020231 L62
theorem e_020232 L63
theorem e_020233 L64
theorem e_020300 L65
theorem e_020301 L66
theorem e_020302 L67
theorem e_020303 L68
theorem e_020310 L69
theorem e_020311 L70
theorem e_020312 L71
theorem e_020313 L72
theorem e_020320 L73
theorem e_020321 L74
theorem e_020322 L75
theorem e_020323 L76
theorem e_020330 L77
theorem e_020331 L78
theorem e_020332 L79
theorem e_020333 L80
theorem e_021000 L81
theorem e_021001 L82
theorem e_021002 L83
theorem e_021003 L84
theorem e_021010 L85
theorem e_021011 L86
theorem e_021012 L87
theorem e_021013 L88
theorem e_021020 L89
theorem e_021021 L90
theorem e_021022 L91
theorem e_021023 L92
theorem e_021030 L93
theorem e_021031 L94
theorem e_021032 L95
theorem e_021033 L96

… and 176 more