Skip to content

[Merged by Bors] - chore: move mul_ite, add dite version, multiplicativise ite_add_ite#17963

Closed
YaelDillies wants to merge 3 commits intomasterfrom
ite_mul_ite
Closed

[Merged by Bors] - chore: move mul_ite, add dite version, multiplicativise ite_add_ite#17963
YaelDillies wants to merge 3 commits intomasterfrom
ite_mul_ite

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Oct 20, 2024

Open in Gitpod

@YaelDillies YaelDillies mentioned this pull request Oct 20, 2024
Closed
3 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 20, 2024 •
edited
Loading

PR summary 109de5f646

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ dite_div
+ dite_div_dite
+ dite_mul
+ dite_mul_dite
+ div_dite
+ div_ite
+ ite_div
+ ite_div_ite
+ ite_mul_ite
+ mul_dite
- ite_add_ite
- ite_sub_ite

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.

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Oct 20, 2024
b-mehta
b-mehta reviewed Oct 20, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@b-mehta b-mehta left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 20, 2024

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Oct 20, 2024
@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Oct 20, 2024

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Oct 20, 2024
@YaelDillies
chore: move mul_ite, add dite version, multiplicativise `ite_add_…
69bbcb4 
…ite` (#17963)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 20, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: move mul_ite, add dite version, multiplicativise ite_add_ite [Merged by Bors] - chore: move mul_ite, add dite version, multiplicativise ite_add_ite Oct 20, 2024
@mathlib-bors mathlib-bors bot closed this Oct 20, 2024
@mathlib-bors mathlib-bors bot deleted the ite_mul_ite branch October 20, 2024 22:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@b-mehta b-mehta b-mehta left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@YaelDillies @b-mehta