module module

`IndisputableMonolith.Gravity.SevenGaps.ClassPushforward`

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 (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.SevenGaps.FreudenthalTorusClassMass module_import
IndisputableMonolith.Gravity.SevenGaps.QuotientFirstZ module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.PathSumMeasure module_import

declarations in this module (24)

def classFiber L96
theorem mem_classFiber L101
def fiberCard L109
theorem sum_fiberwise_quotient L117
theorem sum_eq_quotient_sum_classMass L129
theorem equivalent_of_mk_eq L152
def classMass L162
theorem classMass_eq_fiberCard_mul_mu L169
theorem does L185
theorem Z_eq_classPushforward L188
theorem zRS_eq_classPushforward L213
abbrev edgeAB L231
abbrev edgeBA L244
def edgeSwapRelabel L255
def firstEndpointVal L267
theorem firstEndpointVal_edgeAB L270
theorem firstEndpointVal_edgeBA L272
theorem edgeAB_ne_edgeBA L276
theorem exists_nonSingleton_fiber L288
theorem one_lt_fiberCard_edgeClass L295
theorem mu_lt_classMass_edgeClass L315
structure ClassPushforwardStatus L333
def classPushforwardStatus L355
theorem classPushforwardStatus_flags L367