module module

`IndisputableMonolith.Cost.Ndim.Connections`

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

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.Ndim.Core module_import

declarations in this module (9)

def delta L20
def xFlatConnection L24
def tPulledConnection L27
def ProjectivelyEquivalentToZeroAt L31
theorem xFlatConnection_apply L36
theorem tPulledConnection_diag L39
theorem tPulledConnection_offDiag L44
theorem projectivelyEquivalent_one_dim L50
theorem not_projectivelyEquivalentToZeroAt_tPulledConnection L59