Triangle Similarity

This file contains theorems about similarity of triangles, including conditions for similarity based on sides and angles.

theorem EuclideanGeometry.similar_of_angle_angle {V₁ : Type u_1} {V₂ : Type u_2} {P₁ : Type u_3} {P₂ : Type u_4} [NormedAddCommGroup V₁] [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₁] [InnerProductSpace ℝ V₂] [MetricSpace P₁] [MetricSpace P₂] [NormedAddTorsor V₁ P₁] [NormedAddTorsor V₂ P₂] {a b c : P₁} {a' b' c' : P₂} (h_not_col : ¬Collinear ℝ {a, b, c}) (h₁ : angle a b c = angle a' b' c') (h₂ : angle b c a = angle b' c' a') : Similar ![a, b, c] ![a', b', c']

If two triangles have two pairs equal angles, then the triangles are similar.

theorem EuclideanGeometry.similar_of_side_angle_side {V₁ : Type u_1} {V₂ : Type u_2} {P₁ : Type u_3} {P₂ : Type u_4} [NormedAddCommGroup V₁] [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₁] [InnerProductSpace ℝ V₂] [MetricSpace P₁] [MetricSpace P₂] [NormedAddTorsor V₁ P₁] [NormedAddTorsor V₂ P₂] {a b c : P₁} {a' b' c' : P₂} (h_not_col : ¬Collinear ℝ {a, b, c}) (h_not_col' : ¬Collinear ℝ {a', b', c'}) (h : angle a b c = angle a' b' c') (hd : dist a b * dist b' c' = dist b c * dist a' b') : Similar ![a, b, c] ![a', b', c']

If two triangles have proportional adjacent sides and an equal included angle, then the triangles are similar.

theorem Similar.angle_eq {V₁ : Type u_1} {V₂ : Type u_2} {P₁ : Type u_3} {P₂ : Type u_4} [NormedAddCommGroup V₁] [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₁] [InnerProductSpace ℝ V₂] [MetricSpace P₁] [MetricSpace P₂] [NormedAddTorsor V₁ P₁] [NormedAddTorsor V₂ P₂] {a b c : P₁} {a' b' c' : P₂} (h : Similar ![a, b, c] ![a', b', c']) : EuclideanGeometry.angle a b c = EuclideanGeometry.angle a' b' c'

For two similar triangles, the corresponding angles are equal.

theorem Similar.angle_eq_all {V₁ : Type u_1} {V₂ : Type u_2} {P₁ : Type u_3} {P₂ : Type u_4} [NormedAddCommGroup V₁] [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₁] [InnerProductSpace ℝ V₂] [MetricSpace P₁] [MetricSpace P₂] [NormedAddTorsor V₁ P₁] [NormedAddTorsor V₂ P₂] {a b c : P₁} {a' b' c' : P₂} (h : Similar ![a, b, c] ![a', b', c']) : EuclideanGeometry.angle a b c = EuclideanGeometry.angle a' b' c' ∧ EuclideanGeometry.angle b c a = EuclideanGeometry.angle b' c' a' ∧ EuclideanGeometry.angle c a b = EuclideanGeometry.angle c' a' b'

In two similar triangles, all three corresponding angles are equal.