mathlib3
9e9c3ab5 - chore(analysis/convex/cone): fix typeclass assumption and add a missing lemma (#15879)

Commit
3 years ago
chore(analysis/convex/cone): fix typeclass assumption and add a missing lemma (#15879) We fix a typeclass assumption: `ordered_add_comm_group` to `add_comm_group`. The ordered structure is never used. Also add a missing lemma: `mem_map`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Author
Parents
Loading