Skip to content

[Merged by Bors] - fix: patch for std4#203 (more sub lemmas for Nat)#6216

Closed
fgdorais wants to merge 2 commits intomasterfrom
fgdorais-nat-sub
Closed

[Merged by Bors] - fix: patch for std4#203 (more sub lemmas for Nat)#6216
fgdorais wants to merge 2 commits intomasterfrom
fgdorais-nat-sub

Conversation

@fgdorais
Copy link
Copy Markdown
Collaborator

@fgdorais fgdorais commented Jul 28, 2023 •
edited
Loading

@fgdorais fgdorais added WIP Work in progress t-number-theory Number theory (also use t-algebra or t-analysis to specialize) t-algebra Algebra (groups, rings, fields, etc) t-order Order theory blocked-by-batt-PR This PR depends on a PR to Batteries labels Jul 28, 2023
@fgdorais fgdorais mentioned this pull request Jul 28, 2023
Merged
1 task
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 28, 2023
@fgdorais fgdorais force-pushed the fgdorais-nat-sub branch 3 times, most recently from f600a4b to ab05ece Compare July 29, 2023 13:26
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 31, 2023
@kim-em kim-em mentioned this pull request Aug 17, 2023
Closed
8 tasks
@fgdorais fgdorais changed the title Fix: patch for std4#203 Fix: patch for std4#203 (more sub lemmas for Nat) Aug 21, 2023
@fgdorais fgdorais changed the title Fix: patch for std4#203 (more sub lemmas for Nat) fix: patch for std4#203 (more sub lemmas for Nat) Aug 21, 2023
@bors bors bot changed the base branch from master to ScottCarnahan/BinomialRing2 September 17, 2023 03:25
@kim-em kim-em changed the base branch from ScottCarnahan/BinomialRing2 to master September 17, 2023 12:14
@ghost ghost 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 1, 2023
@fgdorais fgdorais force-pushed the fgdorais-nat-sub branch 2 times, most recently from a1e987f to d046bba Compare November 1, 2023 03:01
@ghost ghost 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 2, 2023
@fgdorais fgdorais force-pushed the fgdorais-nat-sub branch 2 times, most recently from 29e87f6 to 2ea65e8 Compare November 2, 2023 10:35
@ghost ghost 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 21, 2023
@fgdorais fgdorais force-pushed the fgdorais-nat-sub branch 3 times, most recently from 0042e12 to 6eb8ada Compare November 21, 2023 11:03
@ghost ghost 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 21, 2023
@ghost ghost 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 21, 2023
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 24, 2023
@ghost
Copy link
Copy Markdown

ghost commented Nov 24, 2023

This PR/issue depends on:

@fgdorais fgdorais added awaiting-review and removed WIP Work in progress blocked-by-batt-PR This PR depends on a PR to Batteries t-number-theory Number theory (also use t-algebra or t-analysis to specialize) t-algebra Algebra (groups, rings, fields, etc) t-order Order theory labels Nov 24, 2023
@fgdorais fgdorais requested a review from kim-em November 24, 2023 19:36
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Nov 26, 2023

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Nov 26, 2023
mathlib-bors bot pushed a commit that referenced this pull request Nov 26, 2023
@fgdorais
fix: patch for std4#203 (more sub lemmas for Nat) (#6216)
c159834
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 26, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title fix: patch for std4#203 (more sub lemmas for Nat) [Merged by Bors] - fix: patch for std4#203 (more sub lemmas for Nat) Nov 26, 2023
@mathlib-bors mathlib-bors bot closed this Nov 26, 2023
@mathlib-bors mathlib-bors bot deleted the fgdorais-nat-sub branch November 26, 2023 06:08
awueth pushed a commit that referenced this pull request Dec 19, 2023
@fgdorais @awueth
fix: patch for std4#203 (more sub lemmas for Nat) (#6216)
09b2e81
Shamrock-Frost pushed a commit to Shamrock-Frost/mathlib4 that referenced this pull request Jan 22, 2026
@fgdorais @Shamrock-Frost
fix: patch for std4#203 (more sub lemmas for Nat) (leanprover-commu…
2a22e22 
…nity#6216)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em Awaiting requested review from kim-em

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@fgdorais @kim-em