Commit 2020-08-24 19:17 8af15797

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.)