Erdős problem 633
A triangle whose side lengths and angles are integrally independent is cuttable only into a non-zero square number of congruent triangles. This is proved in [So09c].
Sources
FormalConjectures/ErdosProblems/
633.lean
Retained formal statement
A triangle whose side lengths and angles are integrally independent is cuttable only into a non-zero square number of congruent triangles. This is proved in [So09c].
∀ {n : ℕ} {T : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2))}, LinearIndependent ℤ ![dist (T.points 0) (T.points 1), dist (T.points 1) (T.points 2), dist (T.points 2) (T.points 0)] → LinearIndependent ℤ ![EuclideanGeometry.angle (T.points 0) (T.points 1) (T.points 2), EuclideanGeometry.angle (T.points 1) (T.points 2) (T.points 0), EuclideanGeometry.angle (T.points 2) (T.points 0) (T.points 1)] → (Erdos633.IsCuttable n T ↔ n ≠ 0 ∧ IsSquare n)SolvedStatement only, no proof