Files
elementarGeometrie/ElementarGeometrie.lean
Stefan Kebekus 73aaf8b24a
Some checks failed
Lean Action CI / build (push) Has been cancelled
Working
2026-06-24 13:09:46 +02:00

11 lines
430 B
Lean4

import ElementarGeometrie.Incidence.Basic
import ElementarGeometrie.Incidence.Betweenness
import ElementarGeometrie.Incidence.Congruence
import ElementarGeometrie.Affine.Plane
import ElementarGeometrie.Affine.Desargues
import ElementarGeometrie.Affine.Pappus
import ElementarGeometrie.Projective.Space
import ElementarGeometrie.Projective.Completion
import ElementarGeometrie.Projective.Duality
import ElementarGeometrie.Examples