Rigid motions, congruence and similarity

Lens

MotivationH

Drag, rotate, flip, zoom

Open a photo on a phone. You can drag it across the screen, rotate it, flip it into its mirror image, or pinch to zoom in and out. After the first three moves the picture is exactly the same size and shape as before — only its position has changed. After zooming it is bigger or smaller, but still the same shape: faces are not distorted, and corners keep their angles. Stretching it in one direction only would make everyone look tall and thin.

Tilers in Isfahan and Fez fitting identical star-shaped tiles together, an architect drawing a building at a scale of $1 : 100$ , a surveyor measuring a tree from its shadow: all of them rely on the same precise ideas. Moves that keep shapes identical give us congruence; adding zooms gives us similarity. In the coordinate plane each move becomes a simple formula, and we can prove what each one does.

IntuitionH

Moving a flag around the plane

Think of a small flag: a right triangle with corners $A = (0, 0)$ , $B = (2, 0)$ and $C = (0, 1)$ . It is lopsided on purpose — you can always tell whether it has been flipped. Now move it:

slide it 3 to the right and 1 up: every point moves by the same amount;
turn it a quarter turn about the origin: $B$ swings up to $(0, 2)$ ;
flip it over the $x$ -axis: $C$ drops to $(0, -1)$ , and the flag now points the other way round;
zoom it by a factor of 2 from the origin: $B$ moves out to $(4, 0)$ and $C$ to $(0, 2)$ .

The first three moves never change a length or an angle. The fourth doubles every length, but keeps every angle. And doing moves one after another gives new moves — sometimes surprising ones: two flips can make a turn.

DefinitionsH

Definitions

A transformation of the plane is a rule that sends every point $P$ to a point $P'$ , its image.

Definition— rigid motion (isometry)

A rigid motion, or isometry, is a transformation that preserves distances: for all points $P$ and $Q$ , the distance from $P'$ to $Q'$ equals the distance from $P$ to $Q$ .

Here are the rigid motions we will use, written in coordinates. (Rotations are about the origin and anticlockwise unless we say otherwise.)

Move	Rule
translation by $(a, b)$	$(x, y) \mapsto (x + a,\ y + b)$
rotation by $90^\circ$	$(x, y) \mapsto (-y,\ x)$
rotation by $180^\circ$	$(x, y) \mapsto (-x,\ -y)$
rotation by $270^\circ$ ( $90^\circ$ clockwise)	$(x, y) \mapsto (y,\ -x)$
reflection in the $x$ -axis	$(x, y) \mapsto (x,\ -y)$
reflection in the $y$ -axis	$(x, y) \mapsto (-x,\ y)$
reflection in the line $y = x$	$(x, y) \mapsto (y,\ x)$

Definition— dilation

A dilation with centre $O$ and scale factor $k > 0$ sends each point $P$ to the point $P'$ on the ray from $O$ through $P$ with $OP' = k \cdot OP$ . With centre the origin: $(x, y) \mapsto (kx,\ ky)$ . (The centre itself stays put.)

Definition— congruent and similar

Two figures are congruent if some rigid motion (possibly a sequence of several) maps one exactly onto the other. Two figures are similar if a dilation followed by a rigid motion maps one onto the other.

Definition— composite

Doing a transformation $f$ and then a transformation $g$ is the composite $g \circ f$ (read “ $g$ after $f$ ”): $(g \circ f)(P) = g(f(P))$ . See composition.

Worked examplesH

Worked examples

Example— Images of the flag

Rotate the flag $A = (0, 0)$ , $B = (2, 0)$ , $C = (0, 1)$ by $90^\circ$ : $(x, y) \mapsto (-y, x)$ gives $A' = (0, 0)$ , $B' = (0, 2)$ , $C' = (-1, 0)$ . Then translate by $(3, 1)$ : $A'' = (3, 1)$ , $B'' = (3, 3)$ , $C'' = (2, 1)$ . So the flag is congruent to the triangle with corners $(3, 1)$ , $(3, 3)$ , $(2, 1)$ .

Example— Showing two triangles are similar

Is the flag similar to the triangle $(1, 1)$ , $(1, 5)$ , $(-1, 1)$ ? Its legs are 4 and 2, twice the flag's legs 2 and 1. Dilate by 2: $(0, 0)$ , $(4, 0)$ , $(0, 2)$ . Rotate by $90^\circ$ : $(0, 0)$ , $(0, 4)$ , $(-2, 0)$ . Translate by $(1, 1)$ : $(1, 1)$ , $(1, 5)$ , $(-1, 1)$ . ✓ Similar, with scale factor 2.

Example— Undoing a move

Translation by $(3, 1)$ is undone by translation by $(-3, -1)$ . Rotation by $90^\circ$ is undone by rotation by $270^\circ$ (three more quarter turns make a full turn). Every reflection undoes itself.

Example— Rectangles that are not similar

A $1 \times 2$ rectangle and a $1 \times 3$ rectangle are not similar. A similarity multiplies all lengths by the same $k$ . Matching the short sides needs $k = 1$ , but then the long side $2$ becomes $2$ , not $3$ ; matching the short side of the first to the long side of the second needs $k = 3$ , and then $2$ becomes $6$ , not $1$ . By contrast, any two squares are similar: a square of side $s$ becomes a square of side $t$ under a dilation with $k = t / s$ .

Example— Measuring a tree with its shadow

At the same moment, a pole $1.5$ m tall casts a shadow $2$ m long, and a tree casts a shadow $12$ m long. The sun's rays are parallel, so the pole, its shadow and the ray form a triangle similar to the one formed by the tree: the scale factor is $12 / 2 = 6$ , and the tree is $6 \times 1.5 = 9$ m tall.

ProofH

What the moves keep

We use the distance formula from the Pythagorean theorem: the distance between $P = (x_1, y_1)$ and $Q = (x_2, y_2)$ is $\sqrt{\Delta x^2 + \Delta y^2}$ , where $\Delta x = x_2 - x_1$ and $\Delta y = y_2 - y_1$ . It is enough to compare $\Delta x^2 + \Delta y^2$ .

Theorem— Theorem 1 (these moves are rigid)

Translations, rotations by multiples of $90^\circ$ , and reflections in the axes and in the line $y = x$ are rigid motions.

Proof

Apply each rule to $P$ and $Q$ and look at the differences.

Translation by $(a, b)$ : the differences become $(x_2 + a) - (x_1 + a) = \Delta x$ and $\Delta y$ . Unchanged.
Rotation by $90^\circ$ : $P' = (-y_1, x_1)$ , $Q' = (-y_2, x_2)$ , so the differences become $-\Delta y$ and $\Delta x$ , and $(-\Delta y)^2 + \Delta x^2 = \Delta x^2 + \Delta y^2$ .
Reflection in the $x$ -axis: the differences become $\Delta x$ and $-\Delta y$ , and $(-\Delta y)^2 = \Delta y^2$ .
Reflection in $y = x$ : the differences are swapped, which does not change the sum of their squares.

Rotations by $180^\circ$ and $270^\circ$ are two and three quarter turns, and the reflection in the $y$ -axis is similar to the $x$ -axis case; so these follow too (by Theorem 2 below, or directly).

∎

Theorem— Theorem 2 (composites and inverses)

If $f$ and $g$ are rigid motions, so is the composite $g \circ f$ . If a rigid motion $f$ has an inverse $g$ (a transformation that undoes it), then $g$ is a rigid motion too.

Proof

For any $P$ , $Q$ : the distance from $g(f(P))$ to $g(f(Q))$ equals the distance from $f(P)$ to $f(Q)$ , because $g$ is rigid; and that equals the distance from $P$ to $Q$ , because $f$ is rigid.

For the inverse: since $g$ undoes $f$ , we have $f(g(P)) = P$ and $f(g(Q)) = Q$ . Because $f$ is rigid, the distance from $g(P)$ to $g(Q)$ equals the distance from $f(g(P))$ to $f(g(Q))$ , which is the distance from $P$ to $Q$ .

∎

Theorem— Theorem 3 (rigid motions keep angles)

A rigid motion sends every angle to an angle of the same size. Congruent figures have equal corresponding lengths and equal corresponding angles.

Proof

Take an angle $\angle BAC$ and complete it to the triangle $ABC$ . A rigid motion sends it to a triangle $A'B'C'$ with the same three side lengths. A triangle is fixed by its three sides (the SSS rule: you cannot build two differently shaped triangles from the same three sticks), so the two triangles have the same angles, and $\angle B'A'C' = \angle BAC$ .

∎

Theorem— Theorem 4 (two reflections make a rotation)

Reflecting in a line $\ell_1$ and then in a line $\ell_2$ , where the two lines cross at a point $O$ at an angle $\theta$ (measured anticlockwise from $\ell_1$ to $\ell_2$ ), is the rotation about $O$ by $2\theta$ .

Proof

Both reflections keep the distance from $O$ , since $O$ is on both mirrors. So we only need to follow directions. Measure the direction of a point $P$ as an angle from $\ell_1$ , so that $\ell_2$ is at angle $\theta$ . Reflection in the line at angle $\theta$ sends direction $\psi$ to direction $2\theta - \psi$ (the mirror sits exactly halfway between them). So $P$ , at direction $\varphi$ , goes first to direction $-\varphi$ (reflection in $\ell_1$ , the line at angle $0$ ), and then to direction $2\theta - (-\varphi) = \varphi + 2\theta$ . Every point stays at the same distance from $O$ and turns by $2\theta$ : that is the rotation by $2\theta$ .

∎

For example, the $x$ -axis and the line $y = x$ cross at $45^\circ$ , so reflecting in the $x$ -axis and then in $y = x$ is the rotation by $90^\circ$ : in coordinates, $(x, y) \mapsto (x, -y) \mapsto (-y, x)$ . ✓ In the other order the angle from the first mirror to the second is $-45^\circ$ , and we get the rotation by $-90^\circ$ : $(x, y) \mapsto (y, x) \mapsto (y, -x)$ . Two reflections in the same line give the rotation by $0^\circ$ : nothing moves.

Theorem— Theorem 5 (order matters)

Composing transformations is not commutative: in general, $g \circ f \neq f \circ g$ .

Proof

One counterexample is enough. Let $f$ be the translation by $(1, 0)$ and $g$ the rotation by $90^\circ$ . Then $g(f(0, 0)) = g(1, 0) = (0, 1)$ , but $f(g(0, 0)) = f(0, 0) = (1, 0)$ . The two composites send the origin to different points, so they are different transformations. The two reflections above are another counterexample.

∎

Theorem— Theorem 6 (dilations)

A dilation with scale factor $k > 0$ multiplies every length by $k$ , sends every line segment to a parallel segment, keeps every angle, and multiplies every area by $k^2$ .

Proof

Take the centre to be the origin, so $(x, y) \mapsto (kx, ky)$ . (For another centre, translate it to the origin first, dilate, and translate back; translations change none of these quantities.)

Lengths. The differences become $k\,\Delta x$ and $k\,\Delta y$ , so the distance becomes $\sqrt{k^2 \Delta x^2 + k^2 \Delta y^2} = k\sqrt{\Delta x^2 + \Delta y^2}$ .

Directions. The image segment has the same slope: $\frac{k\,\Delta y}{k\,\Delta x} = \frac{\Delta y}{\Delta x}$ (and vertical segments stay vertical). So each segment is sent to a parallel segment pointing the same way.

Angles. An angle is formed by two rays; their images point in the same two directions, so the angle between them is the same.

Areas. A rectangle $a \times b$ with sides along the axes becomes $ka \times kb$ , with area $k^2 ab$ . A triangle's base and height are both multiplied by $k$ , so its area $\tfrac12 \cdot \text{base} \cdot \text{height}$ is multiplied by $k^2$ . Any polygon can be cut into triangles, so its area is multiplied by $k^2$ too.

∎

So similar figures have the same angles, and corresponding lengths in the same ratio $k$ . Doubling every length makes the area four times as large, and tripling makes it nine times.

Formal mathematicsF

Rigid motions in Lean

Points have rational coordinates, and transformations are functions from points to points. Lengths are compared through d2, the square of the distance, which avoids square roots.

PointLean 4Formally verified

/-- A point of the coordinate plane with rational coordinates. -/
structure Point where
  x : Rat
  y : Rat
deriving DecidableEq

Axioms used: No axiomsformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

d2Lean 4Formally verified

/-- The **square** of the distance from `P` to `Q` (the distance formula without the square
root): `(x₂ - x₁)² + (y₂ - y₁)²`. -/
def d2 (P Q : Point) : Rat := (Q.x - P.x) * (Q.x - P.x) + (Q.y - P.y) * (Q.y - P.y)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

translateLean 4Formally verified

/-- Translation by `(a, b)`: every point moves `a` to the right and `b` up. -/
def translate (a b : Rat) (P : Point) : Point := ⟨P.x + a, P.y + b⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

rot90Lean 4Formally verified

/-- Rotation by `90°` anticlockwise about the origin: `(x, y) ↦ (-y, x)`. -/
def rot90 (P : Point) : Point := ⟨-P.y, P.x⟩

Axioms used: No axiomsformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

rot180Lean 4Formally verified

/-- Rotation by `180°` (a half turn) about the origin: `(x, y) ↦ (-x, -y)`. -/
def rot180 (P : Point) : Point := ⟨-P.x, -P.y⟩

Axioms used: No axiomsformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

reflectXLean 4Formally verified

/-- Reflection in the `x`-axis: `(x, y) ↦ (x, -y)`. -/
def reflectX (P : Point) : Point := ⟨P.x, -P.y⟩

Axioms used: No axiomsformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

reflectDiagLean 4Formally verified

/-- Reflection in the line `y = x`: `(x, y) ↦ (y, x)`. -/
def reflectDiag (P : Point) : Point := ⟨P.y, P.x⟩

Axioms used: No axiomsformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

dilateLean 4Formally verified

/-- Dilation with centre the origin and scale factor `k`: `(x, y) ↦ (kx, ky)`. -/
def dilate (k : Rat) (P : Point) : Point := ⟨k * P.x, k * P.y⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

Theorem 1, one move at a time, then Theorem 2:

IsIsometryLean 4Formally verified

/-- A transformation is a **rigid motion** (an *isometry*) if it keeps the distance between every
two points. We compare squared distances, which is the same thing for lengths `≥ 0`. -/
def IsIsometry (f : Point → Point) : Prop := ∀ P Q : Point, d2 (f P) (f Q) = d2 P Q

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

translate_isometryLean 4Proved here from basic factsFormally verified

/-- A translation is a rigid motion: both coordinates of `Q - P` are unchanged, because the
added `a` (and `b`) cancel. -/
theorem translate_isometry (a b : Rat) : IsIsometry (translate a b) := by
  intro P Q
  unfold d2 translate
  grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

rot90_isometryLean 4Proved here from basic factsFormally verified

/-- A quarter turn is a rigid motion: the differences `(Δx, Δy)` become `(-Δy, Δx)`, and
`(-Δy)² + (Δx)² = (Δx)² + (Δy)²`. -/
theorem rot90_isometry : IsIsometry rot90 := by
  intro P Q
  unfold d2 rot90
  grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

reflectX_isometryLean 4Proved here from basic factsFormally verified

/-- Reflection in the `x`-axis is a rigid motion: `(-Δy)² = (Δy)²`. -/
theorem reflectX_isometry : IsIsometry reflectX := by
  intro P Q
  unfold d2 reflectX
  grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

reflectDiag_isometryLean 4Proved here from basic factsFormally verified

/-- Reflection in the line `y = x` is a rigid motion: it swaps `Δx` and `Δy`. -/
theorem reflectDiag_isometry : IsIsometry reflectDiag := by
  intro P Q
  unfold d2 reflectDiag
  grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

isometry_compLean 4Proved here from basic factsFormally verified

/-- **The composite of two rigid motions is a rigid motion.** If `f` and `g` keep distances, so
does "first `f`, then `g`": `d(g(f P), g(f Q)) = d(f P, f Q) = d(P, Q)`. -/
theorem isometry_comp {f g : Point → Point} (hf : IsIsometry f) (hg : IsIsometry g) :
    IsIsometry (g ∘ f) := by
  intro P Q
  calc d2 ((g ∘ f) P) ((g ∘ f) Q) = d2 (g (f P)) (g (f Q)) := rfl
    _ = d2 (f P) (f Q) := hg (f P) (f Q)
    _ = d2 P Q := hf P Q

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

isometry_inverseLean 4Proved here from basic factsFormally verified

/-- **The inverse of a rigid motion is a rigid motion.** If `g` undoes `f` (`f (g P) = P` for
every `P`) and `f` keeps distances, then `g` keeps distances:
`d(g P, g Q) = d(f (g P), f (g Q)) = d(P, Q)`. -/
theorem isometry_inverse {f g : Point → Point} (hf : IsIsometry f)
    (hfg : ∀ P, f (g P) = P) : IsIsometry g := by
  intro P Q
  calc d2 (g P) (g Q) = d2 (f (g P)) (f (g Q)) := (hf (g P) (g Q)).symm
    _ = d2 P Q := by rw [hfg P, hfg Q]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

translate_undoLean 4Proved here from basic factsFormally verified

/-- Translating by `(a, b)` is undone by translating by `(-a, -b)`. -/
theorem translate_undo (a b : Rat) (P : Point) :
    translate (-a) (-b) (translate a b P) = P := by
  cases P
  simp only [translate, Point.mk.injEq]
  constructor <;> grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

rot90_fourLean 4Proved here from basic factsFormally verified

/-- Four quarter turns make a full turn: every point comes back. So the inverse of `rot90` is
`rot90` applied three times (a quarter turn clockwise). -/
theorem rot90_four (P : Point) : rot90 (rot90 (rot90 (rot90 P))) = P := by
  cases P
  simp only [rot90, Point.mk.injEq]
  constructor <;> grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

rot90_twiceLean 4Proved here from basic factsFormally verified

/-- Two quarter turns make a half turn. -/
theorem rot90_twice (P : Point) : rot90 (rot90 P) = rot180 P := rfl

Axioms used: No axiomsformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

Composing: Theorem 4 for the two mirrors at $45^\circ$ , in both orders, and the counterexample of Theorem 5.

two_reflections_rotationLean 4Proved here from basic factsFormally verified

/-- **Two reflections make a rotation.** Reflecting in the `x`-axis and then in the line `y = x`
(two mirrors meeting at `45°`) is the rotation by `90°`, twice the angle between the mirrors:
`(x, y) ↦ (x, -y) ↦ (-y, x)`. -/
theorem two_reflections_rotation (P : Point) : reflectDiag (reflectX P) = rot90 P := rfl

Axioms used: No axiomsformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

reflections_other_orderLean 4Proved here from basic factsFormally verified

/-- In the other order the two reflections give the rotation by `90°` **clockwise**, which is
`rot90` done three times: `(x, y) ↦ (y, x) ↦ (y, -x)`. -/
theorem reflections_other_order (P : Point) :
    reflectX (reflectDiag P) = rot90 (rot90 (rot90 P)) := by
  cases P
  simp only [reflectX, reflectDiag, rot90, Point.mk.injEq]
  constructor <;> grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

order_mattersLean 4Proved here from basic factsFormally verified

/-- **Order matters.** Translating `1` to the right and then turning a quarter turn sends the
origin to `(0, 1)`; turning first and then translating sends it to `(1, 0)`. -/
theorem order_matters :
    rot90 (translate 1 0 ⟨0, 0⟩) ≠ translate 1 0 (rot90 ⟨0, 0⟩) := by decide +kernel

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

Angles. Instead of measuring angles in degrees, Lean works with the dot product $(B - A) \cdot (C - A)$ , which records the angle at $A$ together with the two side lengths. The identity dot_from_sides is the precise form of “a triangle is fixed by its three sides”, and it proves Theorem 3 for every rigid motion:

dotAtLean 4Formally verified

/-- The dot product of the sides `AB` and `AC` of the angle at `A`:
`(B - A) · (C - A)`. It is `0` exactly for a right angle, positive for an acute angle and
negative for an obtuse one; together with the two side lengths it fixes the angle. -/
def dotAt (A B C : Point) : Rat :=
  (B.x - A.x) * (C.x - A.x) + (B.y - A.y) * (C.y - A.y)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

dot_from_sidesLean 4Proved here from basic factsFormally verified

/-- The angle at `A` is determined by the three side lengths of triangle `ABC`:
`2 · (B - A)·(C - A) = AB² + AC² - BC²`. (This is the coordinate form of "a triangle is fixed by
its three sides".) -/
theorem dot_from_sides (A B C : Point) :
    2 * dotAt A B C = d2 A B + d2 A C - d2 B C := by
  unfold dotAt d2
  grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

isometry_preserves_anglesLean 4Proved here from basic factsFormally verified

/-- **Rigid motions keep angles.** A rigid motion keeps the three side lengths of every triangle,
so by `dot_from_sides` it keeps the dot product that records the angle at `A`. -/
theorem isometry_preserves_angles {f : Point → Point} (hf : IsIsometry f) (A B C : Point) :
    dotAt (f A) (f B) (f C) = dotAt A B C := by
  have h1 := dot_from_sides (f A) (f B) (f C)
  have h2 := dot_from_sides A B C
  rw [hf A B, hf A C, hf B C] at h1
  grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

Dilations (Theorem 6), with the non-example that a dilation is not rigid, and signed area, which also detects whether a move flips the plane over:

dilate_d2Lean 4Proved here from basic factsFormally verified

/-- **A dilation multiplies lengths by `k`**: squared distances are multiplied by `k²`. -/
theorem dilate_d2 (k : Rat) (P Q : Point) : d2 (dilate k P) (dilate k Q) = k * k * d2 P Q := by
  unfold d2 dilate
  grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

dilate_not_isometryLean 4Proved here from basic factsFormally verified

/-- A non-example: the dilation with factor `2` is **not** a rigid motion. It moves `(1, 0)` to
`(2, 0)`, doubling its distance from the origin. -/
theorem dilate_not_isometry : ¬ IsIsometry (dilate 2) := by
  intro h
  have := h ⟨0, 0⟩ ⟨1, 0⟩
  revert this
  decide +kernel

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

dilate_dotLean 4Proved here from basic factsFormally verified

/-- A dilation multiplies the dot product at every angle by `k²`, the same factor as the
squared lengths of both sides. So the *shape* of every angle (the dot product compared with the
lengths) is unchanged: **dilations keep angles**. -/
theorem dilate_dot (k : Rat) (A B C : Point) :
    dotAt (dilate k A) (dilate k B) (dilate k C) = k * k * dotAt A B C := by
  unfold dotAt dilate
  grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

signedArea2Lean 4Formally verified

/-- Twice the **signed area** of triangle `ABC`: positive when `A → B → C` goes anticlockwise,
negative when clockwise. (Its size is twice the ordinary area.) -/
def signedArea2 (A B C : Point) : Rat :=
  (B.x - A.x) * (C.y - A.y) - (C.x - A.x) * (B.y - A.y)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

dilate_areaLean 4Proved here from basic factsFormally verified

/-- **A dilation multiplies areas by `k²`.** Doubling all lengths makes areas four times as
large. -/
theorem dilate_area (k : Rat) (A B C : Point) :
    signedArea2 (dilate k A) (dilate k B) (dilate k C) = k * k * signedArea2 A B C := by
  unfold signedArea2 dilate
  grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

rot90_areaLean 4Proved here from basic factsFormally verified

/-- A quarter turn keeps signed area: it keeps both size and orientation. -/
theorem rot90_area (A B C : Point) :
    signedArea2 (rot90 A) (rot90 B) (rot90 C) = signedArea2 A B C := by
  unfold signedArea2 rot90
  grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

reflectX_areaLean 4Proved here from basic factsFormally verified

/-- A reflection keeps the size of the area but **reverses orientation**: the signed area
changes sign, so anticlockwise triangles become clockwise ones. This is why no sequence of
slides and turns can produce a mirror image. -/
theorem reflectX_area (A B C : Point) :
    signedArea2 (reflectX A) (reflectX B) (reflectX C) = -signedArea2 A B C := by
  unfold signedArea2 reflectX
  grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

Finally congruence and similarity for triangles, the two worked examples, and the rectangles:

CongruentLean 4Formally verified

/-- Triangle `ABC` is **congruent** to triangle `A'B'C'` if some rigid motion sends `A, B, C` to
`A', B', C'`. -/
def Congruent (A B C A' B' C' : Point) : Prop :=
  ∃ f : Point → Point, IsIsometry f ∧ f A = A' ∧ f B = B' ∧ f C = C'

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

congruent_exampleLean 4Proved here from basic factsFormally verified

/-- The triangle `(0, 0), (2, 0), (0, 1)` is congruent to `(3, 1), (3, 3), (2, 1)`: turn a quarter
turn about the origin, then translate by `(3, 1)`. -/
theorem congruent_example : Congruent ⟨0, 0⟩ ⟨2, 0⟩ ⟨0, 1⟩ ⟨3, 1⟩ ⟨3, 3⟩ ⟨2, 1⟩ :=
  ⟨translate 3 1 ∘ rot90, isometry_comp rot90_isometry (translate_isometry 3 1),
    by decide +kernel, by decide +kernel, by decide +kernel⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

SimilarLean 4Formally verified

/-- Triangle `ABC` is **similar** to triangle `A'B'C'` if a dilation with some factor `k > 0`
followed by a rigid motion sends `A, B, C` to `A', B', C'`. -/
def Similar (A B C A' B' C' : Point) : Prop :=
  ∃ k : Rat, 0 < k ∧ ∃ f : Point → Point, IsIsometry f ∧
    f (dilate k A) = A' ∧ f (dilate k B) = B' ∧ f (dilate k C) = C'

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

similar_exampleLean 4Proved here from basic factsFormally verified

/-- The triangle `(0, 0), (2, 0), (0, 1)` is similar to `(1, 1), (1, 5), (-1, 1)`: dilate by `2`,
turn a quarter turn, then translate by `(1, 1)`. -/
theorem similar_example : Similar ⟨0, 0⟩ ⟨2, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 5⟩ ⟨-1, 1⟩ :=
  ⟨2, by decide +kernel, translate 1 1 ∘ rot90,
    isometry_comp rot90_isometry (translate_isometry 1 1),
    by decide +kernel, by decide +kernel, by decide +kernel⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

congruent_preserves_d2Lean 4Proved here from basic factsFormally verified

/-- Congruent triangles have equal corresponding sides (here `AB = A'B'`; the other two sides are
the same argument). -/
theorem congruent_preserves_d2 {A B C A' B' C' : Point} (h : Congruent A B C A' B' C') :
    d2 A' B' = d2 A B := by
  obtain ⟨f, hf, hA, hB, _⟩ := h
  rw [← hA, ← hB]
  exact hf A B

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

rectangles_not_similarLean 4Proved here from basic factsFormally verified

/-- **Not all rectangles are similar.** A `1 × 2` rectangle and a `1 × 3` rectangle cannot be
matched by one scale factor: `k · 1 = 1` forces `k = 1`, but then `k · 2 = 2 ≠ 3`; and matching
the sides the other way round, `k · 1 = 3` forces `k = 3`, but then `k · 2 = 6 ≠ 1`. -/
theorem rectangles_not_similar :
    ¬ ∃ k : Rat, (k * 1 = 1 ∧ k * 2 = 3) ∨ (k * 1 = 3 ∧ k * 2 = 1) := by
  intro ⟨k, h⟩
  rcases h with ⟨h1, h2⟩ | ⟨h1, h2⟩ <;> grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RigidMotionsSimilarity.leanTry it in the Lean web editor

What is not formalised here: Theorem 4 for mirrors at an arbitrary angle (it needs reflections in arbitrary lines, which bring in square roots or trigonometry), the SSS rule in its geometric form, and the fact that areas of all shapes scale by $k^2$ (we prove it for triangles via signed area). Mathlib has rigid motions as Isometry and AffineIsometryEquiv, and dilations as homothety.

ComputationC

Composing symmetries, measuring dilations

Composing the eight grid symmetriesPythonExact computationExhaustive finite checkComputationally tested

"""The eight grid symmetries: composing turns and flips, exhaustively.

Four rotations about the origin (by 0, 90, 180 and 270 degrees) and four
reflections (in the x-axis, the y-axis and the lines y = x and y = -x) all
send grid points to grid points. The experiment composes every pair of them,
identifies each result by its effect on the points (1, 0) and (0, 1), and
prints the composition table. From the table it reads off: composites stay
in the set (closure), every move has an undo, two reflections always give a
rotation, and the order of composition often matters. It also checks on a
grid that all eight keep distances. Exact and exhaustive for these 8 moves.
"""

#: Each move as a function of (x, y), with its mirror angle or turn angle.
MOVES = {
    "R0": lambda x, y: (x, y),
    "R90": lambda x, y: (-y, x),
    "R180": lambda x, y: (-x, -y),
    "R270": lambda x, y: (y, -x),
    "Mx": lambda x, y: (x, -y),     # mirror: the x-axis (angle 0)
    "Md": lambda x, y: (y, x),      # mirror: y = x (angle 45)
    "My": lambda x, y: (-x, y),     # mirror: the y-axis (angle 90)
    "Ma": lambda x, y: (-y, -x),    # mirror: y = -x (angle 135)
}
MIRROR_ANGLE = {"Mx": 0, "Md": 45, "My": 90, "Ma": 135}
NAMES = list(MOVES)

def signature(f):
    """Images of (1, 0) and (0, 1); a linear move is fixed by these two."""
    return (f(1, 0), f(0, 1))

def name_of(f):
    """The name of the move with the same effect as f."""
    sig = signature(f)
    for name, g in MOVES.items():
        if signature(g) == sig:
            return name
    return None

def then(first, second):
    """The composite: do ``first``, then ``second``."""
    f, g = MOVES[first], MOVES[second]
    return lambda x, y: g(*f(x, y))

def table():
    """table[(a, b)] = name of 'a, then b'."""
    return {(a, b): name_of(then(a, b)) for a in NAMES for b in NAMES}

def keeps_distances(f, radius=3):
    """True if f keeps squared distances between all grid points."""
    pts = [(x, y) for x in range(-radius, radius + 1)
           for y in range(-radius, radius + 1)]
    for p in pts:
        for q in pts:
            fp, fq = f(*p), f(*q)
            d_before = (p[0] - q[0]) ** 2 + (p[1] - q[1]) ** 2
            d_after = (fp[0] - fq[0]) ** 2 + (fp[1] - fq[1]) ** 2
            if d_before != d_after:
                return False
    return True

def main():
    t = table()
    print("Composition table: row = first move, column = second move")
    print("      " + "".join(f"{b:>6}" for b in NAMES))
    for a in NAMES:
        print(f"{a:>6}" + "".join(f"{t[(a, b)]:>6}" for b in NAMES))
    print()
    closed = all(v is not None for v in t.values())
    undo = all(any(t[(a, b)] == "R0" for b in NAMES) for a in NAMES)
    print(f"Every composite is one of the eight: {closed}")
    print(f"Every move has an undo among the eight: {undo}")
    mirrors = list(MIRROR_ANGLE)
    twice = all(
        t[(m1, m2)] == f"R{(2 * (MIRROR_ANGLE[m2] - MIRROR_ANGLE[m1])) % 360}"
        for m1 in mirrors for m2 in mirrors)
    print("Mirror m1 then mirror m2 = rotation by 2 x (angle m2 - angle m1):"
          f" {twice}")
    pairs = [(a, b) for i, a in enumerate(NAMES) for b in NAMES[i + 1:]]
    differ = [(a, b) for a, b in pairs if t[(a, b)] != t[(b, a)]]
    print(f"Pairs of different moves where the order matters: {len(differ)}"
          f" of {len(pairs)}")
    print(f"  e.g. Mx then Md = {t[('Mx', 'Md')]}, but Md then Mx ="
          f" {t[('Md', 'Mx')]}")
    print(f"All eight keep distances on a 7 x 7 grid: "
          f"{all(keeps_distances(f) for f in MOVES.values())}")
    print()
    print("Epistemic status: exact and exhaustive for these eight moves. The")
    print("two-mirrors rule is proved in the lesson for mirrors at any angle;")
    print("here it is checked only for mirrors at multiples of 45 degrees.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The table shows Theorems 2, 4 and 5 at work on a finite set of moves, exhaustively: every composite is again one of the eight, every move has an undo, flip-then-flip is always a turn by twice the angle between the mirrors, and for 12 of the 28 pairs the order matters. These eight moves form the symmetry group of the square.

Dilations change sizes, not shapesPythonExact computationNumerical approximationComputationally tested

"""Dilations: what changes and what stays the same, measured on 200 triangles.

The experiment makes 200 triangles with seeded random whole-number vertices
and applies dilations with scale factors 1/2, 2 and 3 (centre the origin, and
also centre (2, -1)). With exact fractions it checks that every squared side
length is multiplied by k^2, every area by k^2, and every side keeps its
direction (its slope). It also measures the angles numerically and checks they
do not change. A horizontal-only stretch is the non-example: it changes
angles. Finally it uses similar triangles to measure a tree from its shadow.
"""

import math
import random
from fractions import Fraction

def dilate(p, k, centre=(0, 0)):
    """Dilation with the given centre and scale factor k."""
    cx, cy = centre
    return (cx + k * (p[0] - cx), cy + k * (p[1] - cy))

def stretch_x(p, k):
    """Non-example: stretch horizontally only, (x, y) -> (kx, y)."""
    return (k * p[0], p[1])

def sq_len(p, q):
    """Squared distance between two points."""
    return (q[0] - p[0]) ** 2 + (q[1] - p[1]) ** 2

def area(tri):
    """Area of a triangle by the shoelace formula (exact for fractions)."""
    (ax, ay), (bx, by), (cx, cy) = tri
    return Fraction(abs((bx - ax) * (cy - ay) - (cx - ax) * (by - ay))) / 2

def angles(tri):
    """The three angles of a triangle in degrees (numerical)."""
    out = []
    for i in range(3):
        a, b, c = tri[i], tri[(i + 1) % 3], tri[(i + 2) % 3]
        u = (b[0] - a[0], b[1] - a[1])
        v = (c[0] - a[0], c[1] - a[1])
        dot = u[0] * v[0] + u[1] * v[1]
        cos = dot / math.sqrt((u[0] ** 2 + u[1] ** 2) * (v[0] ** 2 + v[1] ** 2))
        out.append(math.degrees(math.acos(max(-1.0, min(1.0, float(cos))))))
    return out

def parallel(p, q, p2, q2):
    """True if segment p2q2 is parallel to (has the same direction as) pq."""
    return (q[0] - p[0]) * (q2[1] - p2[1]) == (q[1] - p[1]) * (q2[0] - p2[0])

def random_triangles(count, seed=1872):
    """Non-degenerate triangles with whole-number vertices from -9 to 9."""
    rng = random.Random(seed)
    tris = []
    while len(tris) < count:
        tri = [(rng.randint(-9, 9), rng.randint(-9, 9)) for _ in range(3)]
        if area(tri) != 0:
            tris.append(tri)
    return tris

def check(tris, k, centre):
    """Counts of triangles passing each test for one dilation."""
    lengths = areas = directions = angle_ok = 0
    for tri in tris:
        img = [dilate(p, k, centre) for p in tri]
        sides = [(i, (i + 1) % 3) for i in range(3)]
        lengths += all(sq_len(img[i], img[j]) == k * k * sq_len(tri[i], tri[j])
                       for i, j in sides)
        areas += area(img) == k * k * area(tri)
        directions += all(parallel(tri[i], tri[j], img[i], img[j])
                          for i, j in sides)
        angle_ok += all(abs(x - y) < 1e-9
                        for x, y in zip(angles(tri), angles(img)))
    return lengths, areas, directions, angle_ok

def main():
    tris = random_triangles(200)
    print("200 random triangles; dilation results (number of triangles passing)")
    print(f"{'k':>4} {'centre':>8} {'len^2 x k^2':>12} {'area x k^2':>11}"
          f" {'parallel':>9} {'angles':>7}")
    for k in (Fraction(1, 2), Fraction(2), Fraction(3)):
        for centre in ((0, 0), (2, -1)):
            res = check(tris, k, centre)
            print(f"{str(k):>4} {str(centre):>8}" + f"{res[0]:>13}{res[1]:>12}"
                  f"{res[2]:>10}{res[3]:>8}")
    changed = sum(any(abs(x - y) > 1e-6 for x, y in
                      zip(angles(t), angles([stretch_x(p, 2) for p in t])))
                  for t in tris)
    print(f"Non-example: stretching x by 2 changed the angles of {changed} of"
          " 200 triangles.")
    print()
    pole, pole_shadow, tree_shadow = 1.5, 2.0, 12.0
    k = tree_shadow / pole_shadow
    print(f"Shadows: a {pole} m pole casts {pole_shadow} m, a tree {tree_shadow} m;"
          f" k = {k:g},")
    print(f"so the tree is {k:g} x {pole} = {k * pole:g} m tall (similar triangles).")
    print()
    print("Epistemic status: lengths, areas and directions are checked exactly")
    print("for these 1200 triangle-dilation pairs; angles are compared")
    print("numerically. This is evidence, not proof; the lesson proves that every")
    print("dilation behaves this way.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Lengths, areas and directions are checked exactly with fractions; angles are compared numerically. The horizontal stretch is a useful non-example: it changes the angles of every triangle tested, so it is not a similarity. None of this proves Theorem 6 — 200 triangles are not all triangles — but it would have caught a wrong statement such as “areas are multiplied by $k$ ”.

Explore

Explore: build a transformation

The blue triangle is the flag $A = (0, 0)$ , $B = (2, 0)$ , $C = (0, 1)$ . Its image $A'B'C'$ is made by four moves in this order: dilate by $k$ , flip in the $x$ -axis if $m = -1$ , turn about the origin by the chosen angle, then slide by $(h, v)$ .

Challenges: (1) Move the image exactly onto the triangle $T$ with corners $(3, 1)$ , $(3, 3)$ , $(2, 1)$ , using $k = 1$ . That proves the flag and $T$ are congruent. (2) Now find settings that send the flag to $(1, 1)$ , $(1, 5)$ , $(-1, 1)$ (watch the labels $A'$ , $B'$ , $C'$ ). (3) With $m = -1$ , can you ever make the image land on $T$ with $A'$ , $B'$ , $C'$ on the corresponding corners? Why not? (Hint: look at the order of the letters going round.)

Dilate, flip, turn, slide

A point moves along the curve as t changes: x and y are both functions of t.

the flag ABC
its image A′B′C′

dilate: scale factor kk = 1flip: m = −1 reflects in the x-axism = 1turn: angle in degreesang = 0slide right by hh = 0slide up by vv = 0

Move along tt = 0.38

(0.75, 0)
(0.75, 0)

Two reflections as matrices: the first matrix below is the reflection in the $x$ -axis, the second the reflection in the line $y = x$ . The widget shows both orders of composing them. Check that each composite is a rotation (no flip in the little flag, determinant $+1$ ), and that the two orders turn in opposite directions.

Two mirrors make a turn

Apply A and then B, or B and then A, and compare the results.

A =

Set A to:

B =

Set B to:

First A, then B: the matrix BA

BA =

0−110

First B, then A: the matrix AB

AB =

01−10

image of the grid
image of the unit square
image of the flag
before the transformation
after the first step

AB ≠ BA: the order matters.

BA means “apply A first, then B”: products of transformations are read from right to left.

det(AB) = det(BA) = det A · det B = −1 · −1 = 1 The area scale factor is the same in either order.

Exercises

1. Rigid motions, congruence and similarity

Warm-upHuman

Rotate the point $(2, 5)$ by $90^\circ$ anticlockwise about the origin. Where does it land?

Choose one

(-5, 2)

(5, -2)

(5, 2)

(-2, -5)

2. Rigid motions, congruence and similarity

Warm-upHuman

Translate the point $(1, -1)$ by $(-3, 4)$ . Where does it land?

Choose one

(-2, 3)

(4, -5)

(-3, -4)

(3, -2)

3. Rigid motions, congruence and similarity

CoreHuman

A shape is reflected in the $x$ -axis and then in the $y$ -axis. Which single move has the same effect?

Choose one

Rotation by

180^\circ

about the originRotation by

90^\circ

about the originReflection in the line

y = x

Nothing — the shape returns to where it started

4. Rigid motions, congruence and similarity

CoreHuman

A triangle has area $5\ \mathrm{cm}^2$ . It is dilated with scale factor $3$ . What is the area of the image, in $\mathrm{cm}^2$ ?

5. Rigid motions, congruence and similarity

CoreHuman

Triangle $P$ has corners $(0, 0)$ , $(3, 0)$ , $(0, 4)$ . Triangle $Q$ has corners $(0, 0)$ , $(6, 0)$ , $(0, 8)$ . Which is true?

Choose one

They are similar but not congruent.They are congruent.They are neither similar nor congruent.They are congruent and similar.

6. Rigid motions, congruence and similarity

CoreHuman

Which of these does every rigid motion keep the same? (Choose all that apply.)

Choose all that apply

7. Rigid motions, congruence and similarity

CoreHuman

Where does the point $(1, 1)$ go if you first translate by $(2, 0)$ and then rotate by $180^\circ$ about the origin?

Choose one

(-3, -1)

(1, -1)

(3, 1)

(-1, -1)

8. Rigid motions, congruence and similarity

StretchHuman

Two mirror lines cross at a point $O$ at an angle of $30^\circ$ . A shape is reflected in the first line and then in the second. The result is a rotation about $O$ . By how many degrees?

9. Rigid motions, congruence and similarity

CoreFormal

In the Lean file, IsIsometry f means that f keeps all distances, and g ∘ f means “first f, then g”. Which statement says that the composite of two rigid motions is a rigid motion?

Choose one

IsIsometry f → IsIsometry g → IsIsometry (g ∘ f)IsIsometry (g ∘ f) → IsIsometry fIsIsometry f → IsIsometry g → g ∘ f = f ∘ gIsIsometry f ∧ IsIsometry g

10. Rigid motions, congruence and similarity

StretchComputational

Points are pairs (x, y). Complete then(f, g) so that it returns a new function that applies f first and then g. Use it to check that reflecting in the $x$ -axis and then in the line $y = x$ is the rotation by $90^\circ$ , and that the other order is not.

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

“Similar figures must be the same size.” That is congruent. Similar figures have the same shape — the same angles and proportional sides — but may differ in size: every photo enlargement is similar to the original.

Misconception

“Any two rectangles are similar.” Rectangles all have four right angles, but their sides need not be in the same ratio: $1 \times 2$ and $1 \times 3$ are not similar. Equal angles are enough for triangles to be similar, but not for quadrilaterals.

Misconception

“The order of transformations never matters.” Turning and then sliding usually differs from sliding and then turning (Theorem 5), and two reflections in crossing lines turn one way or the other depending on the order. Some pairs do commute — two translations, or two rotations about the same centre — but you must check.

Misconception

“Doubling the lengths doubles the area.” A dilation with factor $k$ multiplies areas by $k^2$ : doubling every length makes the area four times as big. (And volumes of solids are multiplied by $k^3$ .)

Misconception

“A reflection is just a rotation viewed differently.” A reflection reverses orientation: an anticlockwise $A \to B \to C$ becomes clockwise, and the signed area changes sign. No sequence of translations and rotations can do that, so a left hand and a right hand are congruent only if reflections are allowed.

ViewpointsH

Other ways of seeing

Algebra— Moves form groups

Theorem 2 says that the rigid motions of the plane can be composed, that composing is associative, that “do nothing” is a rigid motion, and that every rigid motion has an inverse that is again rigid. These are exactly the rules of a group. The eight grid symmetries of the computation form a smaller group with 8 elements, the symmetry group of a square; its four rotations alone form a cyclic group that behaves exactly like addition modulo 4 (see clock arithmetic). Because $g \circ f \ne f \circ g$ in general, these groups are non-commutative — a feature that check-digit designers have even put to work (see check digits). See groups.

Geometry— A geometry is what its moves keep

In 1872 Felix Klein proposed that a geometry is the study of the properties that a group of transformations leaves unchanged. Euclidean geometry studies what rigid motions keep: lengths, angles, areas. Similarity geometry allows dilations too, and keeps only angles and ratios of lengths — which is why a map and the land it shows have “the same geometry” in that sense. Allowing even more transformations gives affine and projective geometry, where angles stop mattering but straight lines remain straight. See transformation geometry.

Category theory— Maps that preserve structure

The plane with its distances is a mathematical structure, and rigid motions are exactly the maps that preserve it. Composites of structure-preserving maps preserve structure, and so do identity maps (Theorem 2) — the two rules that define a category. Dilations preserve less (only ratios), so they belong to a different, larger category. Asking “which maps preserve this structure?” is one of the guiding questions of modern mathematics; see structure-preserving maps.

History & global context

History and global context

Greece. In Euclid's Elements (about 300 BCE), the proof of Book I, Proposition 4 (side–angle–side congruence) imagines placing one triangle on top of another — an early, informal use of rigid motion. Later writers report that Thales measured the height of a pyramid from its shadow by similar triangles; the story is told centuries after his time.
China. Liu Hui's Sea Island Mathematical Manual (263 CE) shows how to find the height of a distant island and its distance using two poles and similar triangles — practical surveying without ever reaching the island.
The Islamic world. Craftsmen across North Africa, Iran and Central Asia built geometric tilings whose patterns repeat under translations, rotations and reflections, such as those of the Alhambra in Granada (14th century) and of buildings in Isfahan.
Modern times. Felix Klein's Erlangen programme (1872) put transformations at the centre of geometry. In 1891 Evgraf Fedorov in Russia proved that there are exactly 17 essentially different symmetry types of repeating wallpaper patterns.

Drag, rotate, flip, zoom

Moving a flag around the plane

Definitions

Worked examples

What the moves keep

Rigid motions in Lean

Composing symmetries, measuring dilations

Explore: build a transformation

Exercises

Common misconceptions

Other ways of seeing

History and global context

Further reading