def EuclidGeom.Triangle.IsIsoceles {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tri : EuclidGeom.Triangle P) : Prop

Equations

• EuclidGeom.Triangle.IsIsoceles tri = (tri.edge₂.length = tri.edge₃.length)

theorem EuclidGeom.is_isoceles_tri_iff_ang_eq_ang_of_nd_tri {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tri_nd : EuclidGeom.TriangleND P) : EuclidGeom.Triangle.IsIsoceles ↑tri_nd ↔ tri_nd.angle₂.value = tri_nd.angle₃.value

theorem EuclidGeom.Triangle.is_isoceles_of_flip_vert_isoceles {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tri : EuclidGeom.Triangle P} (h : EuclidGeom.Triangle.IsIsoceles tri) : EuclidGeom.Triangle.IsIsoceles tri.flip_vertices

def EuclidGeom.Triangle.IsRegular {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tri : EuclidGeom.Triangle P) : Prop

Equations

• EuclidGeom.Triangle.IsRegular tri = (tri.edge₁.length = tri.edge₂.length ∧ tri.edge₁.length = tri.edge₃.length)

theorem EuclidGeom.Triangle.isoceles_of_regular {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tri : EuclidGeom.Triangle P) (h : EuclidGeom.Triangle.IsRegular tri) : EuclidGeom.Triangle.IsIsoceles tri

theorem EuclidGeom.Triangle.regular_of_regular_flip_vert {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tri : EuclidGeom.Triangle P) (h : EuclidGeom.Triangle.IsRegular tri) : EuclidGeom.Triangle.IsRegular tri.flip_vertices

theorem EuclidGeom.Triangle.regular_of_regular_perm_vert {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tri : EuclidGeom.Triangle P) (h : EuclidGeom.Triangle.IsRegular tri) : EuclidGeom.Triangle.IsRegular tri.perm_vertices

theorem EuclidGeom.regular_tri_iff_eq_angle_of_nd_tri {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tri_nd : EuclidGeom.TriangleND P) : EuclidGeom.Triangle.IsRegular ↑tri_nd ↔ tri_nd.angle₁.value = tri_nd.angle₂.value ∧ tri_nd.angle₁.value = tri_nd.angle₃.value

theorem EuclidGeom.ang_eq_sixty_deg_of_cclock_regular_tri {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tri_nd : EuclidGeom.TriangleND P) (cclock : tri_nd.is_cclock) (h : EuclidGeom.Triangle.IsRegular ↑tri_nd) : tri_nd.angle₁.value = ∠[Real.pi / 3] ∧ tri_nd.angle₂.value = ∠[Real.pi / 3] ∧ tri_nd.angle₃.value = ∠[Real.pi / 3]

theorem EuclidGeom.ang_eq_sixty_deg_of_acclock_regular_tri {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tri_nd : EuclidGeom.TriangleND P) (acclock : ¬tri_nd.is_cclock) (h : EuclidGeom.Triangle.IsRegular ↑tri_nd) : tri_nd.angle₁.value = ∠[-Real.pi / 3] ∧ tri_nd.angle₂.value = ∠[-Real.pi / 3] ∧ tri_nd.angle₃.value = ∠[-Real.pi / 3]

theorem EuclidGeom.regular_tri_of_isoceles_tri_of_fst_ang_eq_sixty_deg {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tri_nd : EuclidGeom.TriangleND P) (h : tri_nd.angle₁.value = ∠[Real.pi / 3] ∨ tri_nd.angle₁.value = ∠[-Real.pi / 3]) (h1 : EuclidGeom.Triangle.IsIsoceles ↑tri_nd) : EuclidGeom.Triangle.IsRegular ↑tri_nd

theorem EuclidGeom.regular_tri_of_isoceles_tri_of_snd_ang_eq_sixty_deg {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tri_nd : EuclidGeom.TriangleND P) (h : tri_nd.angle₂.value = ∠[Real.pi / 3] ∨ tri_nd.angle₂.value = ∠[-Real.pi / 3]) (h1 : EuclidGeom.Triangle.IsIsoceles ↑tri_nd) : EuclidGeom.Triangle.IsRegular ↑tri_nd

theorem EuclidGeom.regular_tri_of_isoceles_tri_of_trd_ang_eq_sixty_deg {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tri_nd : EuclidGeom.TriangleND P) (h : tri_nd.angle₃.value = ∠[Real.pi / 3] ∨ tri_nd.angle₃.value = ∠[-Real.pi / 3]) (h1 : EuclidGeom.Triangle.IsIsoceles ↑tri_nd) : EuclidGeom.Triangle.IsRegular ↑tri_nd