Skip to content

[Merged by Bors] - feat port: Data.Int.Cast.Field#1016

Closed
ChrisHughes24 wants to merge 3 commits intomasterfrom
Data.Int.Cast.Field
Closed

[Merged by Bors] - feat port: Data.Int.Cast.Field#1016
ChrisHughes24 wants to merge 3 commits intomasterfrom
Data.Int.Cast.Field

Conversation

@ChrisHughes24
Copy link
Copy Markdown
Member

@ChrisHughes24 ChrisHughes24 commented Dec 14, 2022

ee0c179cd3c8a45aa5bffbf1b41d8dbede452865

@ChrisHughes24 ChrisHughes24 added awaiting-review mathlib-port This is a port of a theory file from mathlib. labels Dec 14, 2022
fpvandoorn
fpvandoorn reviewed Dec 14, 2022
View reviewed changes
Copy link
Copy Markdown
Member

@fpvandoorn fpvandoorn left a comment

Choose a reason for hiding this comment

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

Thanks

bors d+

Mathlib/Data/Int/Cast/Field.lean Outdated
`R = ℤ` and cause nontermination.)
-/
@[norm_cast]
theorem cast_neg_nat_cast {R} [Field R] (n : ℕ) : ((-n : ℤ) : R) = -n := by simp
Copy link
Copy Markdown
Member

@fpvandoorn fpvandoorn Dec 14, 2022

Choose a reason for hiding this comment

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

Suggested change
theorem cast_neg_nat_cast {R} [Field R] (n : ℕ) : ((-n : ℤ) : R) = -n := by simp
theorem cast_neg_natCast {R} [Field R] (n : ℕ) : ((-n : ℤ) : R) = -n := by simp

also in align below

Mathlib/Data/Int/Cast/Field.lean Outdated

/-- Auxiliary lemma for norm_cast to move the cast `-↑n` upwards to `↑-↑n`.

(The restriction to `field` is necessary, otherwise this would also apply in the case where
Copy link
Copy Markdown
Member

@fpvandoorn fpvandoorn Dec 14, 2022

Choose a reason for hiding this comment

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

Suggested change
(The restriction to `field` is necessary, otherwise this would also apply in the case where
(The restriction to `Field` is necessary, otherwise this would also apply in the case where

@bors
Copy link
Copy Markdown

bors bot commented Dec 14, 2022

✌️ ChrisHughes24 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 Dec 14, 2022
@ChrisHughes24
Copy link
Copy Markdown
Member Author

ChrisHughes24 commented Dec 14, 2022

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Dec 14, 2022
bors bot pushed a commit that referenced this pull request Dec 14, 2022
@ChrisHughes24
feat port: Data.Int.Cast.Field (#1016)
61138ea 
ee0c179cd3c8a45aa5bffbf1b41d8dbede452865
@bors
Copy link
Copy Markdown

bors bot commented Dec 14, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat port: Data.Int.Cast.Field [Merged by Bors] - feat port: Data.Int.Cast.Field Dec 14, 2022
@bors bors bot closed this Dec 14, 2022
@bors bors bot deleted the Data.Int.Cast.Field branch December 14, 2022 16:04
@github-actions github-actions bot mentioned this pull request Dec 14, 2022
Closed
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Dec 15, 2022
@j-loreaux
chore(*): add mathlib4 synchronization comments (#17943)
a59dad5 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.euclidean_domain.basic`: leanprover-community/mathlib4#919
* `algebra.field.basic`: leanprover-community/mathlib4#975
* `algebra.group.opposite`: leanprover-community/mathlib4#912
* `algebra.group.prod`: leanprover-community/mathlib4#968
* `algebra.group.with_one.units`: leanprover-community/mathlib4#955
* `algebra.group_power.ring`: leanprover-community/mathlib4#979
* `algebra.hom.equiv.type_tags`: leanprover-community/mathlib4#943
* `algebra.hom.ring`: leanprover-community/mathlib4#958
* `algebra.invertible`: leanprover-community/mathlib4#930
* `algebra.order.field.canonical.basic`: leanprover-community/mathlib4#1018
* `algebra.order.field.canonical.defs`: leanprover-community/mathlib4#985
* `algebra.order.field.inj_surj`: leanprover-community/mathlib4#1017
* `algebra.order.group.densely_ordered`: leanprover-community/mathlib4#956
* `algebra.order.group.min_max`: leanprover-community/mathlib4#933
* `algebra.order.group.prod`: leanprover-community/mathlib4#1026
* `algebra.order.group.with_top`: leanprover-community/mathlib4#946
* `algebra.order.hom.monoid`: leanprover-community/mathlib4#944
* `algebra.order.monoid.prod`: leanprover-community/mathlib4#987
* `algebra.order.monoid.to_mul_bot`: leanprover-community/mathlib4#1024
* `algebra.order.ring.abs`: leanprover-community/mathlib4#929
* `algebra.order.ring.cone`: leanprover-community/mathlib4#935
* `algebra.order.sub.basic`: leanprover-community/mathlib4#936
* `algebra.order.sub.with_top`: leanprover-community/mathlib4#932
* `algebra.order.with_zero`: leanprover-community/mathlib4#903
* `combinatorics.quiver.arborescence`: leanprover-community/mathlib4#997
* `combinatorics.quiver.cast`: leanprover-community/mathlib4#990
* `control.traversable.lemmas`: leanprover-community/mathlib4#948
* `data.bool.set`: leanprover-community/mathlib4#960
* `data.int.cast.field`: leanprover-community/mathlib4#1016
* `data.int.cast.lemmas`: leanprover-community/mathlib4#995
* `data.int.cast.prod`: leanprover-community/mathlib4#1015
* `data.int.div`: leanprover-community/mathlib4#1011
* `data.int.dvd.basic`: leanprover-community/mathlib4#996
* `data.int.order.basic`: leanprover-community/mathlib4#938
* `data.nat.cast.basic`: leanprover-community/mathlib4#980
* `data.nat.cast.prod`: leanprover-community/mathlib4#1010
* `data.nat.cast.with_top`: leanprover-community/mathlib4#1019
* `data.nat.gcd.basic`: leanprover-community/mathlib4#965
* `data.nat.order.basic`: leanprover-community/mathlib4#907
* `data.nat.order.lemmas`: leanprover-community/mathlib4#927
* `data.nat.set`: leanprover-community/mathlib4#961
* `data.nat.upto`: leanprover-community/mathlib4#1020
* `data.pequiv`: leanprover-community/mathlib4#1008
* `data.set.basic`: leanprover-community/mathlib4#892
* `data.set.bool_indicator`: leanprover-community/mathlib4#988
* `data.set.image`: leanprover-community/mathlib4#949
* `data.set.n_ary`: leanprover-community/mathlib4#969
* `data.set.opposite`: leanprover-community/mathlib4#983
* `data.set.prod`: leanprover-community/mathlib4#1004
* `data.set.sigma`: leanprover-community/mathlib4#982
* `data.set_like.basic`: leanprover-community/mathlib4#993
* `data.two_pointing`: leanprover-community/mathlib4#984
* `logic.embedding.set`: leanprover-community/mathlib4#986
* `logic.equiv.embedding`: leanprover-community/mathlib4#1021
* `order.directed`: leanprover-community/mathlib4#963
* `order.rel_iso.set`: leanprover-community/mathlib4#1005
* `order.well_founded`: leanprover-community/mathlib4#970
* `ring_theory.coprime.basic`: leanprover-community/mathlib4#899



Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@fpvandoorn fpvandoorn fpvandoorn 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. 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.

3 participants

@ChrisHughes24 @fpvandoorn @kim-em