module module

`IndisputableMonolith.Geometry.DihedralCofactorFormula`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.DihedralCayleyMenger module_import
IndisputableMonolith.Geometry.GramCayleyMenger module_import

declarations in this module (80)

def adjacentFaceOppositeVertices L33
def coordEdgeVector L42
theorem coordEdgeVector_dot_eq_inner L47
theorem coordEdgeVector_eq_base_sub L56
theorem coordEdgeVector_dot_base_sub L63
def faceNormal L71
theorem faceNormal_dot_faceNormal L75
theorem faceNormal_dot_self L86
def geometricDihedralNumerator L97
def geometricDihedralDenomSq L103
def geometricDihedralCos L113
theorem geometricDihedralNumerator_cross L117
theorem geometricDihedralNumerator_edge0_gram L131
theorem cmCofactor3_edge0_eq_four_geometricNumerator L141
theorem faceNormal_edge0_left_self_gram L153
theorem faceNormal_edge0_right_self_gram L160
theorem cmCofactor3_edge0_left_diag_eq_neg_four_normalSq L168
theorem cmCofactor3_edge0_right_diag_eq_neg_four_normalSq L181
theorem cmCofactor3_edge0_diag_product_eq_sixteen_denomSq L194
theorem dotProduct_self_nonneg L205
theorem geometricDihedralDenomSq_nonneg L210
theorem abs_dot_div_sqrt_self_mul_self_le_one L217
theorem geometricDihedralCos_range L244
theorem geometricDihedralCos_interior_of_ne_endpoints L253
theorem cmCofactor3_edge0_sqrt_diag_product L263
theorem geometricDihedralCos_edge0_eq_cofactorRatio_of_sqrt L276
theorem geometricDihedralCos_edge0_eq_cmCofactorRatio L292
theorem geometricDihedralNumerator_edge1_gram L299
theorem cmCofactor3_edge1_eq_four_geometricNumerator L307
theorem faceNormal_edge1_left_self_gram L317
theorem faceNormal_edge1_right_self_gram L323
theorem cmCofactor3_edge1_left_diag_eq_neg_four_normalSq L330
theorem cmCofactor3_edge1_right_diag_eq_neg_four_normalSq L342
theorem cmCofactor3_edge1_diag_product_eq_sixteen_denomSq L353
theorem cmCofactor3_edge1_sqrt_diag_product L363
theorem geometricDihedralCos_edge1_eq_cmCofactorRatio L374
theorem geometricDihedralNumerator_edge2_gram L386
theorem cmCofactor3_edge2_eq_four_geometricNumerator L394
theorem faceNormal_edge2_left_self_gram L405
theorem faceNormal_edge2_right_self_gram L411
theorem cmCofactor3_edge2_left_diag_eq_neg_four_normalSq L418
theorem cmCofactor3_edge2_right_diag_eq_neg_four_normalSq L430
theorem cmCofactor3_edge2_diag_product_eq_sixteen_denomSq L441
theorem cmCofactor3_edge2_sqrt_diag_product L451
theorem geometricDihedralCos_edge2_eq_cmCofactorRatio L462
theorem geometricDihedralNumerator_edge3_gram L474
theorem cmCofactor3_edge3_eq_four_geometricNumerator L490
theorem faceNormal_edge3_left_self_gram L500
theorem faceNormal_edge3_right_self_gram L511
theorem cmCofactor3_edge3_left_diag_eq_neg_four_normalSq L528
theorem cmCofactor3_edge3_right_diag_eq_neg_four_normalSq L539
theorem cmCofactor3_edge3_diag_product_eq_sixteen_denomSq L550
theorem cmCofactor3_edge3_sqrt_diag_product L560
theorem geometricDihedralCos_edge3_eq_cmCofactorRatio L571
theorem geometricDihedralNumerator_edge4_gram L583
theorem cmCofactor3_edge4_eq_four_geometricNumerator L599
theorem faceNormal_edge4_left_self_gram L609
theorem faceNormal_edge4_right_self_gram L620
theorem cmCofactor3_edge4_left_diag_eq_neg_four_normalSq L637
theorem cmCofactor3_edge4_right_diag_eq_neg_four_normalSq L648
theorem cmCofactor3_edge4_diag_product_eq_sixteen_denomSq L659
theorem cmCofactor3_edge4_sqrt_diag_product L669
theorem geometricDihedralCos_edge4_eq_cmCofactorRatio L680
theorem geometricDihedralNumerator_edge5_gram L692
theorem cmCofactor3_edge5_eq_four_geometricNumerator L708
theorem faceNormal_edge5_left_self_gram L718
theorem faceNormal_edge5_right_self_gram L729
theorem cmCofactor3_edge5_left_diag_eq_neg_four_normalSq L746
theorem cmCofactor3_edge5_right_diag_eq_neg_four_normalSq L757
theorem cmCofactor3_edge5_diag_product_eq_sixteen_denomSq L768
theorem cmCofactor3_edge5_sqrt_diag_product L778
theorem geometricDihedralCos_edge5_eq_cmCofactorRatio L789
def BergerCofactorFormula3 L800
theorem geometricDihedralCos_eq_cmCofactorRatio L805
theorem bergerCofactorFormula3 L817
theorem dihedralCos3Sq_sqEdgeOfPoints_range L821
theorem dihedralCos3Sq_sqEdgeOfPoints_interior_of_ne_endpoints L829
theorem dihedralCos3_range_of_realization L840
def dihedralAngleData3_of_realization L850
theorem dihedralCos3_interior_of_realization_ne_endpoints L859