module module

`IndisputableMonolith.Geometry.CofactorDerivatives`

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.DihedralDerivatives module_import
IndisputableMonolith.Geometry.ReggeActionSmoothness module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.CofactorPolynomial module_import
IndisputableMonolith.Geometry.DihedralCayleyMenger module_import
IndisputableMonolith.Geometry.RealisabilityCone module_import

declarations in this module (34)

def cmCofactor3FDeriv L29
theorem hasFDerivAt_cmCofactor3 L34
theorem hasDerivAt_div L41
theorem hasDerivAt_dihedralCos3Sq_along L53
theorem hasDerivAt_dihedralDenom3_along L73
def dihedralDenom3DerivValue L106
def dihedralCos3SqDerivValue L114
def dihedralNumeratorClosedDeriv L131
def dihedralLeftDiagClosedDeriv L137
def dihedralRightDiagClosedDeriv L142
def dihedralDenom3ClosedDerivValue L147
def dihedralCos3SqClosedFormDeriv L155
def dihedralDenom3Poly L165
def dihedralCofactorProductPoly L172
def dihedralCofactorNumeratorPoly L178
def dihedralCos3SqPoly L184
def dihedralDenom3PolyClosedDerivValue L188
def dihedralCos3SqPolyClosedFormDeriv L196
theorem dihedralDenom3_eq_poly L203
theorem dihedralCos3Sq_eq_poly L208
theorem dihedralDenom3ClosedDerivValue_eq_poly L214
theorem dihedralCos3SqClosedFormDeriv_eq_poly L222
theorem dihedralCofactorPoly_discriminant_eq L232
theorem dihedralDenom3Poly_sq L240
theorem one_sub_dihedralCos3SqPoly_sq_eq L249
theorem sqrt_one_sub_dihedralCos3SqPoly_sq_eq L271
theorem dihedralCofactorProductPoly_pos_of_nonDegenerate L285
theorem dihedralCofactorProductPoly_nonneg_of_nonDegenerate L299
theorem dihedralCofactorProductPoly_ne_zero_of_nonDegenerate L304
theorem dihedralDenom3Poly_pos_of_nonDegenerate L309
theorem dihedralDenom3Poly_ne_zero_of_nonDegenerate L317
theorem dihedralCos3SqClosedFormDeriv_eq_generic L324
theorem hasDerivAt_dihedralCos3Sq_from_cofactors L335
theorem hasDerivAt_dihedralCos3Sq_explicit L363