mathlib

df6a0b2e - feat(analysis/convex/body): define bodies and implement module instance (#16297)

feat(analysis/convex/body): define bodies and implement module instance (#16297) Defines the type `convex_body V` and endows it with a module structure over the nonnegative reals. This commit also introduces `set_like` and `inhabited` instances. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>