Skip to content

feat: port algebra.ring.basic#830

Merged
kim-em merged 13 commits intomasterfrom
mcdoll/ring_basic
Dec 4, 2022
Merged

feat: port algebra.ring.basic#830
kim-em merged 13 commits intomasterfrom
mcdoll/ring_basic

Conversation

@mcdoll
Copy link
Copy Markdown
Member

@mcdoll mcdoll commented Dec 3, 2022 •
edited
Loading

mathlib SHA: 70d50ecfd4900dd6d328da39ab7ebd516abe4025

@mcdoll mcdoll added help-wanted The author needs attention to resolve issues awaiting-review labels Dec 3, 2022
@mcdoll mcdoll added the mathlib-port This is a port of a theory file from mathlib. label Dec 3, 2022
@hrmacbeth
Copy link
Copy Markdown
Member

hrmacbeth commented Dec 3, 2022 •
edited
Loading

  • I've removed a bit0 lemma.

I believe the current advice is to keep it with

set_option linter.deprecated false in
@[deprecated] lemma my_bit0_lemma ...

see #771 (comment)

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Dec 3, 2022

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Dec 3, 2022
@Ruben-VandeVelde Ruben-VandeVelde removed the help-wanted The author needs attention to resolve issues label Dec 3, 2022
@github-actions github-actions bot mentioned this pull request Dec 4, 2022
Closed
@bryangingechen
Copy link
Copy Markdown
Contributor

bryangingechen commented Dec 4, 2022

bors r+

@kim-em kim-em merged commit 9f19a1b into master Dec 4, 2022
@bors bors bot deleted the mcdoll/ring_basic branch December 4, 2022 02:00
rosborn added a commit that referenced this pull request Dec 4, 2022
@rosborn
Merge branch 'master' into CategoryTheory.Functor.FullyFaithful
a57ac3a 
* master:
  chore: parallelize testing in CI (#845)
  feat: Match mathlib#17801 (#839)
  feat: Match mathlib#16761 (#840)
  feat: port CategoryTheory.NatIso (#820)
  feat: port algebra.ring.basic (#830)
  feat: port Combinatorics.Quiver.ConnectedComponent (#836)
  chore: bump to nightly-2022-12-03 (#838)
@github-actions github-actions bot mentioned this pull request Dec 6, 2022
Open
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Dec 6, 2022
@jcommelin
chore(*): add mathlib4 synchronization comments (#17806)
8770c84 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.divisibility.basic`: leanprover-community/mathlib4#833
* `algebra.group.with_one.defs`: leanprover-community/mathlib4#841
* `algebra.hom.commute`: leanprover-community/mathlib4#831
* `algebra.hom.group`: leanprover-community/mathlib4#659
* `algebra.hom.units`: leanprover-community/mathlib4#745
* `algebra.ring.basic`: leanprover-community/mathlib4#830
* `category_theory.natural_isomorphism`: leanprover-community/mathlib4#820
* `combinatorics.quiver.connected_component`: leanprover-community/mathlib4#836
* `combinatorics.quiver.subquiver`: leanprover-community/mathlib4#828



Co-authored-by: Johan Commelin <johan@commelin.net>
@github-actions github-actions bot mentioned this pull request Dec 19, 2022
Closed
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

mathlib-port This is a port of a theory file from mathlib. 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.

6 participants

@mcdoll @hrmacbeth @kim-em @bryangingechen @Ruben-VandeVelde @digama0