Documentation

EuclideanGeometry.Foundation.Construction.Triangle.Centroid

source
def EuclidGeom.TriangleND.Median1 {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) :
EuclidGeom.SegND P
Equations
Instances For
    source
    structure EuclidGeom.IsCentroid {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) (G : P) :
    Prop
      Instances For
        source
        def EuclidGeom.TriangleND.Centroid {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) :
        P
        Equations
        Instances For
          source
          theorem EuclidGeom.TriangleND.centroid_is_centroid {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) :
          EuclidGeom.IsCentroid tr_nd (EuclidGeom.TriangleND.Centroid tr_nd)