Mathlib v3 is deprecated. Go to Mathlib v4

Theorem orientation.oangle_map_complex

Modification history

2022-10-24 11:01

src/geometry/euclidean/oriented_angle.lean

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

Added orientation.oangle_map_complex View on Github →