Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-30 21:28 2fb109f0

View on Github →

feat(analysis/inner_product/orientation, geometry/euclidean/oriented_angle): use bundled orthonormal bases (#16475) Bundled orthonormal bases (as opposed to bases with a mixin predicate orthonormal) were defined in #12060, and some of the use cases were switched over in #12253. This PR completes the job, switching to bundled orthonormal bases in inner_product/orientation and euclidean/oriented_angle as well as in one remaining construction (the standard -orthonormal basis of ) in inner_product/pi_L2. Formalized as part of the Sphere Eversion project. The part that I will be using in future PRs is the bundled version of the construction orthonormal_basis.adjust_to_orientation in inner_product/orientation.

Estimated changes

deleted theorem orthonormal.conj_lie_symm
deleted theorem orthonormal.det_conj_lie
deleted theorem orthonormal.det_rotation
deleted def orthonormal.oangle
deleted theorem orthonormal.oangle_add
deleted theorem orthonormal.oangle_map
deleted theorem orthonormal.oangle_rev
deleted theorem orthonormal.oangle_self
deleted theorem orthonormal.rotation_pi
deleted theorem orthonormal.rotation_symm
deleted theorem orthonormal.rotation_zero