mathlib3
a08db7e9 - feat(analysis/inner_product_space/two_dim): new file (#16928)

Commit
3 years ago
feat(analysis/inner_product_space/two_dim): new file (#16928) This file defines constructions specific to the geometry of an oriented two-dimensional real inner product space. Main declarations: * `orientation.area_form` * `orientation.right_angle_rotation` * `orientation.kahler` (renaming suggestions are welcome) [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/adding.20angles/near/299839950)
Author
Parents
Loading