Der Satz von Leonardo (englisch Leonardo’s Theorem) ist ein Lehrsatz der Absoluten Geometrie, der dem Mathematiker Hermann Weyl zufolge auf Leonardo da Vinci zurückzuführen ist. Der Satz behandelt die Frage der Struktur endlicher Isometriegruppen absoluter Ebenen.
Der Satz lässt sich in moderner Formulierung angeben wie folgt:

Nach Hermann Weyl entdeckte Leonardo den Satz, als er in seinen Studien zur Architektur der Frage nachging, wie man einem Gebäude Kapellen und Nischen anfügen könne, ohne die Symmetrie des Gebäudekerns zu zerstören.
Der Satz von Leonardo ist Teil einer langen Entwicklung innerhalb der euklidischen Geometrie, in deren Verlauf geometrische Transformationen zunehmend formalisiert wurden. Bereits in den Elementen von Euklid (3. Jh. v. Chr.) erscheinen Bewegungen wie Verschiebungen und Drehungen implizit, jedoch noch ohne explizite Abstraktion des Begriffs der Isometrie.
Einen entscheidenden Wendepunkt markierte das Erlanger Programm von Felix Klein aus dem Jahr 1872, das vorschlug, Geometrien über die Gruppen von Transformationen zu charakterisieren, unter denen bestimmte Eigenschaften invariant bleiben. In diesem Rahmen wird die euklidische Geometrie als die Geometrie der Abstände aufgefasst, deren natürliche Symmetriegruppe die Gruppe aller Isometrien der Ebene ist.
Eine Isometrie der euklidischen Ebene ist eine bijektive Abbildung, die alle Abstände invariant lässt. Formal handelt es sich um eine Abbildung mit für alle Punkte .
Alle Isometrien der Ebene lassen sich eindeutig als Komposition einer Translation und einer orthogonalen Abbildung (also einer Rotation oder Spiegelung) darstellen. Die Gesamtheit aller Isometrien bildet eine Gruppe, die als Halbdirektprodukt der Translationsgruppe mit der orthogonalen Gruppe beschrieben werden kann.
Endliche Untergruppen dieser Isometriegruppe treten als Symmetriegruppen geometrischer Figuren auf, insbesondere regulärer Vielecke. Diese Gruppen lassen sich vollständig klassifizieren und gehören entweder zur Klasse der Zyklische Gruppen oder der Diedergruppen.
Der Satz von Leonardo beschreibt genau diese Klassifikation endlicher Isometriegruppen der Ebene. Er besagt, dass jede endliche Gruppe von ebenen Isometrien entweder ausschließlich aus Drehungen besteht oder zusätzlich Spiegelungen enthält. Im ersten Fall ist die Gruppe isomorph zu einer zyklischen Gruppe, im zweiten Fall zu einer Diedergruppe.
Diese Aussage entspricht geometrisch der Tatsache, dass die Symmetrien regulärer Vielecke entweder nur aus Rotationen um einen gemeinsamen Mittelpunkt bestehen oder zusätzlich Achsenspiegelungen enthalten. Die formale gruppentheoretische Beschreibung erlaubt es, diese Symmetrien vollständig zu erfassen und voneinander zu unterscheiden.
Der algebraische Beweis des Satzes von Leonardo basiert auf der Struktur der Isometriegruppe der euklidischen Ebene. Zunächst zeigt man, dass jede Isometrie entweder orientierungserhaltend oder orientierungsumkehrend ist. Die orientierungserhaltenden Isometrien sind genau die Drehungen um einen Punkt.
Sei eine endliche Gruppe von Isometrien der Ebene. Enthält nur orientierungserhaltende Isometrien, so besteht sie ausschließlich aus Rotationen um einen gemeinsamen Fixpunkt. In diesem Fall ist notwendigerweise eine endliche Untergruppe der Rotationsgruppe und somit zyklisch.
Enthält hingegen eine orientierungsumkehrende Isometrie, etwa eine Spiegelung, so lässt sich zeigen, dass alle orientierungserhaltenden Elemente eine zyklische Untergruppe bilden und dass die Spiegelungen diese Untergruppe durch Konjugation invertieren. Daraus folgt, dass die Struktur einer Diedergruppe besitzt.
Der Satz von Leonardo stellt ein klassisches Beispiel für die Verbindung zwischen geometrischer Anschauung und abstrakter Algebra dar. Er zeigt, wie geometrische Symmetrien vollständig durch gruppentheoretische Methoden beschrieben werden können, und gilt als prototypisches Resultat im Sinne des Erlanger Programms.