Skip to content

[Merged by Bors] - feat: port Algebra.Ring.Defs#655

Closed
Ruben-VandeVelde wants to merge 39 commits intomasterfrom
algebra.ring.defs
Closed

[Merged by Bors] - feat: port Algebra.Ring.Defs#655
Ruben-VandeVelde wants to merge 39 commits intomasterfrom
algebra.ring.defs

Conversation

@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor

@Ruben-VandeVelde Ruben-VandeVelde commented Nov 19, 2022 •
edited
Loading

Tracking mathlib commit: 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

pechersky and others added 21 commits November 8, 2022 22:41
@pechersky
feat: port remaining missing Algebra.GroupWithZero.Defs
b2e3173 
Along with module, class, and some lemma docstrings
I kept the additional later-file defns near the bottom
Turns out this file doesn't rely on the Logic.Nontrivial import
@kim-em
merge
f27a53a
@j-loreaux
Port data.nat.cast.defs
c36c9ff
@j-loreaux
fix breakage due to simp set changes
698f6ec
@j-loreaux
add docstring
51abcf4
@j-loreaux
add import
bd180f5
@j-loreaux
Move Nat.AtLeastTwo earlier in the file.
4824c40
@j-loreaux
reapply simp attribute
007c673
@j-loreaux
Revert "fix breakage due to simp set changes"
7871670 
This reverts commit 698f6ec.
@j-loreaux
fix
261b4f7
@j-loreaux
port data.int.cast.defs
36bbdd9
@j-loreaux
add to import list
daab3bb
@j-loreaux
appease linter?
6417536
@j-loreaux
alphabetize much?
c8aab54
@j-loreaux
oops, fix a few things
53afda5
@Ruben-VandeVelde
Merge remote-tracking branch 'origin/j-loreaux/data.nat.cast.defs' in…
6373859 
…to pechersky/port-group-with-zero-defs
@Ruben-VandeVelde
Remove ad-hoc NoZeroDivisors definition from Positivity (broken)
c735db8
@Ruben-VandeVelde
Partial fix
4739e3b
@Ruben-VandeVelde
Import Algebra/Ring/Defs.lean from mathport
0f3411d
@Ruben-VandeVelde
Initial fixes
0bf8247
@Ruben-VandeVelde
More fixes
1dbb7fc
@Ruben-VandeVelde Ruben-VandeVelde added help-wanted The author needs attention to resolve issues blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Nov 19, 2022
@kim-em kim-em removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 20, 2022
@Ruben-VandeVelde Ruben-VandeVelde added awaiting-review mathlib-port This is a port of a theory file from mathlib. and removed help-wanted The author needs attention to resolve issues labels Nov 20, 2022
@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor Author

Ruben-VandeVelde commented Nov 20, 2022

Thanks for the help, should be ready for review now

kim-em
kim-em reviewed Nov 20, 2022
View reviewed changes
Mathlib/Algebra/Ring/Defs.lean Outdated

variable [AddMonoidWithOne α]

-- TODO: Move to `Data.Nat.Cast.Defs`?
Copy link
Copy Markdown
Contributor

@kim-em kim-em Nov 20, 2022

Choose a reason for hiding this comment

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

👍

kim-em
kim-em reviewed Nov 20, 2022
View reviewed changes
Mathlib/Algebra/Ring/Defs.lean Outdated
#align two_mul two_mul

section deprecated
set_option linter.deprecated false
Copy link
Copy Markdown
Contributor

@kim-em kim-em Nov 20, 2022

Choose a reason for hiding this comment

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

If it's only for one command, you can use

set_option linter.deprecated false in ...

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Nov 20, 2022

Looks good otherwise.

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Nov 20, 2022

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

@kim-em kim-em added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Nov 20, 2022
@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor Author

Ruben-VandeVelde commented Nov 20, 2022

Thanks!

bors r+

bors bot pushed a commit that referenced this pull request Nov 20, 2022
@pechersky @kim-em
@j-loreaux @Ruben-VandeVelde @digama0
feat: port Algebra.Ring.Defs (#655)
085e7ab 
Tracking mathlib commit: [39af7d3bf61a98e928812dbc3e16f4ea8b795ca3](leanprover-community/mathlib3@39af7d3)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Nov 20, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Algebra.Ring.Defs [Merged by Bors] - feat: port Algebra.Ring.Defs Nov 20, 2022
@bors bors bot closed this Nov 20, 2022
@bors bors bot deleted the algebra.ring.defs branch November 20, 2022 21:47
This was referenced Nov 22, 2022
Closed
Closed
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Nov 23, 2022
@eric-wieser
chore(*): add mathlibport comments (#17686)
4afb682 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* leanprover-community/mathlib4#643
* leanprover-community/mathlib4#646
* leanprover-community/mathlib4#648
* leanprover-community/mathlib4#649
* leanprover-community/mathlib4#651
* leanprover-community/mathlib4#655
* leanprover-community/mathlib4#656
* leanprover-community/mathlib4#657
* leanprover-community/mathlib4#661
* leanprover-community/mathlib4#670
* leanprover-community/mathlib4#671
* leanprover-community/mathlib4#672
* leanprover-community/mathlib4#686
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Nov 23, 2022
chore(*): add mathlib4 synchronization comments (#17686)
1044429 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.char_zero.defs`: leanprover-community/mathlib4#661
* `algebra.group.order_synonym`: leanprover-community/mathlib4#651
* `algebra.hierarchy_design`: leanprover-community/mathlib4#657
* `algebra.quotient`: leanprover-community/mathlib4#643
* `algebra.ring.defs`: leanprover-community/mathlib4#655
* `algebra.ring.order_synonym`: leanprover-community/mathlib4#671
* `control.equiv_functor`: leanprover-community/mathlib4#649
* `data.dlist.basic`: leanprover-community/mathlib4#616
* `data.int.cast.basic`: leanprover-community/mathlib4#670
* `data.lazy_list`: leanprover-community/mathlib4#686
* `data.list.lex`: leanprover-community/mathlib4#672
* `data.option.n_ary`: leanprover-community/mathlib4#656
* `data.sigma.lex`: leanprover-community/mathlib4#646
* `group_theory.eckmann_hilton`: leanprover-community/mathlib4#626
* `logic.equiv.basic`: leanprover-community/mathlib4#631
* `order.iterate`: leanprover-community/mathlib4#648
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Nov 24, 2022
chore(*): add mathlib4 synchronization comments (#17686)
fe771af 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.char_zero.defs`: leanprover-community/mathlib4#661
* `algebra.group.inj_surj`: leanprover-community/mathlib4#707
* `algebra.group.order_synonym`: leanprover-community/mathlib4#651
* `algebra.group.units`: leanprover-community/mathlib4#549
* `algebra.hierarchy_design`: leanprover-community/mathlib4#657
* `algebra.quotient`: leanprover-community/mathlib4#643
* `algebra.ring.defs`: leanprover-community/mathlib4#655
* `algebra.ring.order_synonym`: leanprover-community/mathlib4#671
* `control.equiv_functor`: leanprover-community/mathlib4#649
* `data.dlist.basic`: leanprover-community/mathlib4#616
* `data.int.cast.basic`: leanprover-community/mathlib4#670
* `data.lazy_list`: leanprover-community/mathlib4#686
* `data.list.lex`: leanprover-community/mathlib4#672
* `data.option.n_ary`: leanprover-community/mathlib4#656
* `data.sigma.lex`: leanprover-community/mathlib4#646
* `data.ulift`: leanprover-community/mathlib4#703
* `group_theory.eckmann_hilton`: leanprover-community/mathlib4#626
* `logic.equiv.basic`: leanprover-community/mathlib4#631
* `order.iterate`: leanprover-community/mathlib4#648
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Nov 25, 2022
chore(*): add mathlib4 synchronization comments (#17686)
cb1d279 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.char_zero.defs`: leanprover-community/mathlib4#661
* `algebra.group.inj_surj`: leanprover-community/mathlib4#707
* `algebra.group.order_synonym`: leanprover-community/mathlib4#651
* `algebra.group.units`: leanprover-community/mathlib4#549
* `algebra.hierarchy_design`: leanprover-community/mathlib4#657
* `algebra.opposites`: leanprover-community/mathlib4#644
* `algebra.quotient`: leanprover-community/mathlib4#643
* `algebra.ring.defs`: leanprover-community/mathlib4#655
* `algebra.ring.order_synonym`: leanprover-community/mathlib4#671
* `control.equiv_functor`: leanprover-community/mathlib4#649
* `data.dlist.basic`: leanprover-community/mathlib4#616
* `data.int.cast.basic`: leanprover-community/mathlib4#670
* `data.lazy_list`: leanprover-community/mathlib4#686
* `data.list.lex`: leanprover-community/mathlib4#672
* `data.option.n_ary`: leanprover-community/mathlib4#656
* `data.sigma.lex`: leanprover-community/mathlib4#646
* `data.ulift`: leanprover-community/mathlib4#703
* `group_theory.eckmann_hilton`: leanprover-community/mathlib4#626
* `logic.equiv.basic`: leanprover-community/mathlib4#631
* `order.iterate`: leanprover-community/mathlib4#648
eric-wieser
eric-wieser reviewed Jan 22, 2023
View reviewed changes
Mathlib/Algebra/Ring/Defs.lean
AddGroupWithOne α
#align non_assoc_ring NonAssocRing

class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser Jan 22, 2023

Choose a reason for hiding this comment

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

This doesn't match the version in Lean 3...

Zulip Thread

Ruben-VandeVelde added a commit that referenced this pull request Jan 22, 2023
@Ruben-VandeVelde
chore: align definition of Ring with mathlib3
2c93835 
I appear to have inadvertantly copied the unaligned ah-hoc definition in #655.
@Ruben-VandeVelde Ruben-VandeVelde mentioned this pull request Jan 22, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@kim-em kim-em kim-em left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). mathlib-port This is a port of a theory file from mathlib.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@Ruben-VandeVelde @kim-em @eric-wieser @pechersky @j-loreaux @digama0