module
module
IndisputableMonolith.Gravity.RecordFluxBoostHeat
show as:
view Lean formalization →
used by (1)
depends on (1)
declarations in this module (8)
-
def
UniformProbeAttachment -
theorem
exteriorStepHeat_cast_eq_sum_channelDelta -
theorem
quadContr_cutEventStress_eq_sq_mul_heat -
def
PostedBoostHeatNormalizationAssumption -
theorem
matchesPostedBoostHeat_of_attachment -
theorem
zero_covectors_fail_nonzero_posted_heat -
structure
RecordFluxBoostHeatCert -
theorem
recordFluxBoostHeatCert