Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-29 02:18 54d1f9bb

View on Github →

refactor(geometry/euclidean/oriented_angle): split file (#17134) Split geometry.euclidean.oriented_angle up into geometry.euclidean.angle.oriented.basic, geometry.euclidean.angle.oriented.affine and geometry.euclidean.angle.sphere (the last only has a few results at present but is intended to get a lot more, both oriented results and unoriented results deduced from the oriented ones).

Estimated changes

added theorem sbtw.oangle_eq_left
added theorem sbtw.oangle_eq_right
added theorem sbtw.oangle_sign_eq
added theorem wbtw.oangle_eq_left
added theorem wbtw.oangle_eq_right
deleted theorem sbtw.oangle_eq_left
deleted theorem sbtw.oangle_eq_left_right
deleted theorem sbtw.oangle_eq_right
deleted theorem sbtw.oangle_sign_eq
deleted theorem sbtw.oangle_sign_eq_left
deleted theorem sbtw.oangle_sign_eq_right
deleted theorem wbtw.oangle_eq_left
deleted theorem wbtw.oangle_eq_right