mathlib3
f333194f - feat(geometry/euclidean/oriented_angle): refactor to a basis-free definition (#16596)

Commit
3 years ago
feat(geometry/euclidean/oriented_angle): refactor to a basis-free definition (#16596) Zulip: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/adding.20angles
Author
Parents
Loading