Theorems · Theorem · geometry

EuclideanGeometry.similar_of_side_angle_side

∀ {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [inst : NormedAddCommGroup V₁]
  [inst_1 : NormedAddCommGroup V₂] [inst_2 : InnerProductSpace ℝ V₁] [inst_3 : InnerProductSpace ℝ V₂]
  [inst_4 : MetricSpace P₁] [inst_5 : MetricSpace P₂] [inst_6 : NormedAddTorsor V₁ P₁] [inst_7 : NormedAddTorsor V₂ P₂]
  {a b c : P₁} {a' b' c' : P₂},
  ¬Collinear ℝ {a, b, c} →
    ¬Collinear ℝ {a', b', c'} →
      EuclideanGeometry.angle a b c = EuclideanGeometry.angle a' b' c' →
        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.

Defined in

Mathlib.Geometry.Euclidean.Similarity

Cited by

0 results in Mathlib

Foundations

Depth 195 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedAddCommGroupInnerProductSpaceInnerProductSpaceMetricSpaceMetricSpaceNormedAddTorsorNormedAddTorsor