Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: Positivity extension for Finset.prod #10481

Merged
merged 2 commits into from
Feb 13, 2024

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Feb 13, 2024

Followup to #9365


Open in Gitpod

@YaelDillies YaelDillies added blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) awaiting-review t-meta Tactics, attributes or user commands t-algebra Algebra (groups, rings, fields, etc) t-order Order theory labels Feb 13, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@YaelDillies YaelDillies merged commit 40fe08f into positivity_finset_sum Feb 13, 2024
15 checks passed
@mathlib-bors mathlib-bors bot deleted the positivity_finset_prod branch February 13, 2024 21:45
@YaelDillies YaelDillies restored the positivity_finset_prod branch February 14, 2024 12:50
@YaelDillies YaelDillies removed blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) awaiting-review labels Apr 20, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
t-algebra Algebra (groups, rings, fields, etc) t-meta Tactics, attributes or user commands t-order Order theory
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants