module module

`IndisputableMonolith.Foundation.PairKernelDiscreteGauss`

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.MetricEdgeImage4D module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PairKernelLocality module_import

declarations in this module (16)

def IsAntisym L78
def divF L81
def constFlow L90
theorem constFlow_not_antisym L92
theorem constFlow_sum_div L98
theorem constFlow_breaks_conservation L105
theorem antisym_sum_finset_zero L115
theorem sum_divF_zero L138
theorem sum_divF_region_eq_boundary_flux L146
theorem sigma_sum_zero_of_continuity L164
def elementaryPosting L178
theorem elementaryPosting_antisym L181
theorem elementaryPosting_sum_div_zero L190
theorem elementaryPosting_div_source L197
theorem elementaryPosting_div_sink L212
theorem elementaryPosting_divF_eq_unitDipole L232