You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository was archived by the owner on Jul 24, 2024. It is now read-only.
refactor(geometry/euclidean): split up file (#3926)
Split up `geometry/euclidean.lean` into four smaller files in
`geometry/euclidean`. There should be no changes to any of the
individual definitions, or to the set of definitions present, but
module doc strings have been expanded.
Various definitions in `geometry/euclidean/basic.lean` are not used by
all the other files, so it would be possible to split it up further,
but that doesn't seem necessary for now, and more of those things may
be used by more other files in future. (For example,
`geometry/euclidean/circumcenter.lean` doesn't make any use of angles
at present. But a version of the law of sines involving the
circumradius would naturally go in
`geometry/euclidean/circumcenter.lean`, and would introduce such a
dependency.)
0 commit comments