module module

`IndisputableMonolith.Gravity.SevenGaps.FreudenthalTorusClassMass`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.ClassPushforward module_import
IndisputableMonolith.Gravity.SevenGaps.PathSumProbes module_import

declarations in this module (10)

theorem mu_torusClassMember_le L75
theorem norm_freudenthal_labeledSummand_le L89
theorem torus_classMass_eq_fiberCard_mul_mu L107
theorem torus_classMass_le_fiberCard_div_cube L122
theorem one_div_cube_le_one_div L135
theorem tendsto_mu_freudenthal_zero L144
theorem tendsto_labeledSummand_zero L160
structure TorusClassMassStatus L174
def torusClassMassStatus L192
theorem torusClassMassStatus_flags L203