Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-24 11:01 f333194f

View on Github →

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

Estimated changes

added theorem real.angle.cos_add
added theorem real.angle.sin_add
modified theorem orientation.oangle_map
modified theorem orientation.rotation_pi