Commit 2024-01-09 08:14 2b755321
View on Github →chore: Move Bernoulli's inequality (#9456) The first versions for ordered semirings do not need to import so much but:
- they have no obvious place to go
- nobody needs them that early (in particular, it seems nobody needs them without also needing the ordered field version) Part of #9411