module
module
IndisputableMonolith.Geometry.GramCayleyMenger
show as:
view Lean formalization →
used by (1)
depends on (2)
declarations in this module (11)
-
def
sqEdgesFromGram -
theorem
cm3_sqEdgesFromGram_eq_8_det -
def
GramCayleyMengerTheorem -
theorem
sqDist_eq_baseGram -
theorem
sqEdgeOfPoints_eq_sqEdgesFromGram -
theorem
cm3_sqEdgeOfPoints_eq_8_det_gram -
theorem
gram_cayley_menger_realized -
theorem
gramCayleyMengerTheorem -
theorem
gram_cayley_menger_target_equiv -
def
GramCayleyMengerDetTheorem -
theorem
gram_cayley_menger_det_target_equiv