module module

`IndisputableMonolith.Foundation.SimplicialLedger.DirichletAction`

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

declarations in this module (17)

structure WeightedLedgerGraph L25
def laplacian_action L31
def discrete_laplacian L36
def laplacian_pairing L40
def laplacian_bilinear L45
theorem right_weighted_sum_eq_neg_left L52
theorem pairing_eq_left_weighted_sum L85
theorem laplacian_bilinear_eq_pairing L110
theorem laplacian_bilinear_comm L149
theorem laplacian_pairing_comm L159
theorem laplacian_action_eq_pairing L167
theorem double_sum_mul_left L180
theorem laplacian_action_line_expansion L195
def unitDipole L253
theorem sum_mul_unitDipole L257
theorem laplacian_action_eq_potential_drop_of_eq_unitDipole L263
theorem laplacian_action_eq_half_potential_drop_of_two_eq_unitDipole L279