Commit 2020-05-30 07:33 62cb7f2f

feat(geometry/euclidean): Euclidean space (#2852) Define Euclidean affine spaces (not necessarily finite-dimensional), and a corresponding instance for the standard Euclidean space fin n → ℝ. This just defines the type class and the instance, with some other basic geometric definitions and results to be added separately once this is in. I haven't attempted to do anything about the euclidean_space definition in geometry/manifold/real_instances.lean that comes with a comment that it uses the wrong norm. That might better be refactored by someone familiar with the manifold code. By defining Euclidean spaces such that they are defined to be metric spaces, and providing an instance, this probably implicitly gives item 91 "The Triangle Inequality" from the 100-theorems list, if that's taken to have a geometric interpretation as in the Coq version, but it's not very clear how something implicit like that from various different pieces of the library, and where the item on the list could be interpreted in several different ways anyway, should be entered in 100.yaml.