IndisputableMonolith.Geometry.AffineIndepInterior

declarations in this module (28)

• def toEuclidean3 L32
• theorem inner_toEuclidean3 L35
• theorem norm_toEuclidean3_sq L41
• theorem sqrt_dot_self_mul_self_eq_norm_mul_norm L48
• theorem toEuclidean3_smul L57
• theorem smul_of_toEuclidean3_smul L62
• theorem dot_div_sqrt_ne_one_of_linearIndependent L69
• theorem dot_div_sqrt_ne_neg_one_of_linearIndependent L89
• def adjacentFaceNormals L108
• def AdjacentFaceNormalsIndependent L116
• theorem faceNormal_ne_zero_of_edgeVectors_linearIndependent L121
• theorem adjacentFaceNormalsIndependent_iff_cross_ne_zero L130
• theorem adjacentFaceNormalsIndependent_of_cross_ne_zero L139
• theorem shared_edge_face_normals_cross L148
• theorem adjacentFaceNormals_cross_eq_triple_smul_edge L159
• theorem faceNormals_independent_of_triple_ne_zero L173
• theorem scalar_triple_ne_zero_of_linearIndependent L188
• theorem coord_linearIndependent_of_euclidean L202
• theorem adjacentFaceNormalsIndependent_of_triple_ne_zero L213
• theorem basisEdgeVector_linearIndependent L227
• theorem coordEdgeVector_from_base_linearIndependent L258
• theorem edge_opposite_coord_triple_linearIndependent L270
• theorem adjacentFaceNormalsIndependent_of_affineIndependent L420
• theorem geometricDihedralCos_strict_interior_of_faceNormals_independent L429
• theorem dihedralCos3Sq_strict_interior_of_faceNormals_independent L445
• theorem geometricDihedralCos_strict_interior_of_affineIndependent L455
• theorem dihedralCos3Sq_strict_interior_of_affineIndependent L463
• structure RealizedNonDegenerateTet L475