mathlib3

265fe3d8 - feat(analysis/inner_product_space/orientation): volume form (#16487)

feat(analysis/inner_product_space/orientation): volume form (#16487) Construct the volume form, a uniquely-determined top-dimensional alternating form on an oriented real inner product space. Formalized as part of the Sphere Eversion project.