module module

`IndisputableMonolith.Geometry.CayleyMengerDerivatives`

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

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Geometry.ReggeRigorousFoundation module_import
IndisputableMonolith.Geometry.SchlaefliTetrahedron module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.CayleyMengerPolynomial module_import

declarations in this module (32)

def cm3_partial0 L61
def cm3_partial1 L67
def cm3_partial2 L73
def cm3_partial3 L79
def cm3_partial4 L85
def cm3_partial5 L91
def cm3_grad L98
def cm3_quadratic L128
def cm3_cubic L144
def cm3_linear L155
theorem cm3_taylor L162
def singlePerturb L172
theorem singlePerturb_at L175
theorem singlePerturb_ne L179
theorem cm3_update_taylor L187
def cm3_quadratic_coeff L220
def cm3_cubic_coeff L231
theorem cm3_quadratic_singlePerturb L233
theorem cm3_cubic_singlePerturb L239
theorem cm3_update_polyform L252
theorem hasDerivAt_shifted_cubic L267
theorem hasDerivAt_cm3_grad L294
theorem hasDerivAt_cm3_partial0 L312
theorem hasDerivAt_cm3_partial1 L316
theorem hasDerivAt_cm3_partial2 L320
theorem hasDerivAt_cm3_partial3 L324
theorem hasDerivAt_cm3_partial4 L328
theorem hasDerivAt_cm3_partial5 L332
def cm3_hessianDiag L340
def cm3GradientCLM L346
theorem hasFDerivAt_cm3 L350
theorem cm3_update_hessianForm L356