Skip to content

[Merged by Bors] - feat: s ⊆ s ^ n when 1 ∈ s#19538

Closed
YaelDillies wants to merge 1 commit intomasterfrom
subset_pow
Closed

[Merged by Bors] - feat: s ⊆ s ^ n when 1 ∈ s#19538
YaelDillies wants to merge 1 commit intomasterfrom
subset_pow

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Nov 27, 2024 •
edited
Loading

and the product of nontrivial sets is nontrivial.

From GrowthInGroups

Open in Gitpod

@YaelDillies YaelDillies requested a review from b-mehta November 27, 2024 12:14
@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 27, 2024 •
edited
Loading

PR summary cbbc4d906c

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

++ Nontrivial.mul
++ Nontrivial.mul_left
++ Nontrivial.mul_right
++ Nontrivial.pow
++ subset_pow

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 27, 2024
@b-mehta
Copy link
Copy Markdown
Contributor

b-mehta commented Nov 27, 2024

The vast majority of the diff in this PR (ignoring the stuff in the one it depends on) isn't about what's in the title. Could you clarify the title or PR description?

@YaelDillies YaelDillies added the t-algebra Algebra (groups, rings, fields, etc) label Nov 27, 2024
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 27, 2024
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Nov 27, 2024

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 27, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 28, 2024
@YaelDillies
feat: s ⊆ s ^ n when 1 ∈ s
cbbc4d9 
From GrowthInGroups
@YaelDillies YaelDillies mentioned this pull request Nov 28, 2024
Closed
2 tasks
@b-mehta
Copy link
Copy Markdown
Contributor

b-mehta commented Nov 28, 2024

Nice

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Nov 28, 2024
mathlib-bors bot pushed a commit that referenced this pull request Nov 28, 2024
@YaelDillies
feat: s ⊆ s ^ n when 1 ∈ s (#19538)
4e9fa40 
and the product of nontrivial sets is nontrivial.

From GrowthInGroups
@YaelDillies YaelDillies removed the request for review from b-mehta November 28, 2024 20:28
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 28, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: s ⊆ s ^ n when 1 ∈ s [Merged by Bors] - feat: s ⊆ s ^ n when 1 ∈ s Nov 28, 2024
@mathlib-bors mathlib-bors bot closed this Nov 28, 2024
@mathlib-bors mathlib-bors bot deleted the subset_pow branch November 28, 2024 20:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@YaelDillies @b-mehta @mathlib4-dependent-issues-bot @leanprover-community-bot-assistant