[Merged by Bors] - chore: Rename `coe_nat`/`coe_int`/`coe_rat` to `natCast`/`intCast`/`ratCast` #11499

YaelDillies · 2024-03-19T08:50:21Z

This is less exhaustive than its sibling #11486 because edge cases are harder to classify. No fundamental difficulty, just me being a bit fast and lazy.

Reduce the diff of #11203

depends on: [Merged by Bors] - chore: Rename zpow_coe_nat to zpow_natCast #11528
depends on: [Merged by Bors] - chore: Rename cat_coe_nat/cast_coe_int to cast_natCast/cast_intCast #11552
depends on: [Merged by Bors] - chore(Data/Int): Rename coe_nat to natCast #11637

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

fpvandoorn · 2024-03-19T14:16:46Z

Can we add deprecated aliases for the old names? Maybe only some of the main lemmas?

fpvandoorn · 2024-03-19T14:28:13Z

Other than that, I'm very much in favor of this, but the poll is indeed not as one-sided as I would have hoped.

YaelDillies · 2024-03-19T15:15:26Z

I estimate that without automation it would take me several hours to write the deprecated aliases 😦 (and no lemma comes to mind as particularly important)

j-loreaux

LGTM but I would like one more maintainer to sign off since the poll was close.

Mathlib/Data/Polynomial/Basic.lean

Mathlib/Order/Filter/FilterProduct.lean

Mathlib/Order/Filter/Germ.lean

Mathlib/RingTheory/Subsemiring/Basic.lean

eric-wieser

Half way through...

Mathlib/Order/Filter/Germ.lean

Mathlib/Data/Polynomial/Basic.lean

Mathlib/Algebra/Group/ULift.lean

Mathlib/Data/ENNReal/Basic.lean

Mathlib/Data/Int/Cast/Basic.lean

Mathlib/Data/Int/Cast/Lemmas.lean

Mathlib/Data/Nat/Cast/Basic.lean

Mathlib/FieldTheory/Adjoin.lean

Mathlib/FieldTheory/Subfield.lean

Mathlib/NumberTheory/LucasLehmer.lean

…atCast`

…tCast` Reduce the diff of #11499

fpvandoorn · 2024-04-07T17:24:06Z

bors merge
bors d+
I think the deprecations make it fine to not list the renames.

mathlib-bors · 2024-04-07T17:24:08Z

✌️ 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.

…atCast` (#11499) This is less exhaustive than its sibling #11486 because edge cases are harder to classify. No fundamental difficulty, just me being a bit fast and lazy. Reduce the diff of #11203

mathlib-bors · 2024-04-07T18:52:40Z

Pull request successfully merged into master.

Build succeeded:

…tCast` (#11552) Reduce the diff of #11499

Reduce the diff of #11499 ## Renames All in the `Int` namespace: * `ofNat_eq_cast` → `ofNat_eq_natCast` * `cast_eq_cast_iff_Nat` → `natCast_inj` * `natCast_eq_ofNat` → `ofNat_eq_natCast` * `coe_nat_sub` → `natCast_sub` * `coe_nat_nonneg` → `natCast_nonneg` * `sign_coe_add_one` → `sign_natCast_add_one` * `nat_succ_eq_int_succ` → `natCast_succ` * `succ_neg_nat_succ` → `succ_neg_natCast_succ` * `coe_pred_of_pos` → `natCast_pred_of_pos` * `coe_nat_div` → `natCast_div` * `coe_nat_ediv` → `natCast_ediv` * `sign_coe_nat_of_nonzero` → `sign_natCast_of_ne_zero` * `toNat_coe_nat` → `toNat_natCast` * `toNat_coe_nat_add_one` → `toNat_natCast_add_one` * `coe_nat_dvd` → `natCast_dvd_natCast` * `coe_nat_dvd_left` → `natCast_dvd` * `coe_nat_dvd_right` → `dvd_natCast` * `le_coe_nat_sub` → `le_natCast_sub` * `succ_coe_nat_pos` → `succ_natCast_pos` * `coe_nat_modEq_iff` → `natCast_modEq_iff` * `coe_natAbs` → `natCast_natAbs` * `coe_nat_eq_zero` → `natCast_eq_zero` * `coe_nat_ne_zero` → `natCast_ne_zero` * `coe_nat_ne_zero_iff_pos` → `natCast_ne_zero_iff_pos` * `abs_coe_nat` → `abs_natCast` * `coe_nat_nonpos_iff` → `natCast_nonpos_iff` Also rename `Nat.coe_nat_dvd` to `Nat.cast_dvd_cast`

…atCast` (#11499) This is less exhaustive than its sibling #11486 because edge cases are harder to classify. No fundamental difficulty, just me being a bit fast and lazy. Reduce the diff of #11203

…tCast` (#11552) Reduce the diff of #11499

Reduce the diff of #11499 ## Renames All in the `Int` namespace: * `ofNat_eq_cast` → `ofNat_eq_natCast` * `cast_eq_cast_iff_Nat` → `natCast_inj` * `natCast_eq_ofNat` → `ofNat_eq_natCast` * `coe_nat_sub` → `natCast_sub` * `coe_nat_nonneg` → `natCast_nonneg` * `sign_coe_add_one` → `sign_natCast_add_one` * `nat_succ_eq_int_succ` → `natCast_succ` * `succ_neg_nat_succ` → `succ_neg_natCast_succ` * `coe_pred_of_pos` → `natCast_pred_of_pos` * `coe_nat_div` → `natCast_div` * `coe_nat_ediv` → `natCast_ediv` * `sign_coe_nat_of_nonzero` → `sign_natCast_of_ne_zero` * `toNat_coe_nat` → `toNat_natCast` * `toNat_coe_nat_add_one` → `toNat_natCast_add_one` * `coe_nat_dvd` → `natCast_dvd_natCast` * `coe_nat_dvd_left` → `natCast_dvd` * `coe_nat_dvd_right` → `dvd_natCast` * `le_coe_nat_sub` → `le_natCast_sub` * `succ_coe_nat_pos` → `succ_natCast_pos` * `coe_nat_modEq_iff` → `natCast_modEq_iff` * `coe_natAbs` → `natCast_natAbs` * `coe_nat_eq_zero` → `natCast_eq_zero` * `coe_nat_ne_zero` → `natCast_ne_zero` * `coe_nat_ne_zero_iff_pos` → `natCast_ne_zero_iff_pos` * `abs_coe_nat` → `abs_natCast` * `coe_nat_nonpos_iff` → `natCast_nonpos_iff` Also rename `Nat.coe_nat_dvd` to `Nat.cast_dvd_cast`

…atCast` (#11499) This is less exhaustive than its sibling #11486 because edge cases are harder to classify. No fundamental difficulty, just me being a bit fast and lazy. Reduce the diff of #11203

…tCast` (#11552) Reduce the diff of #11499

Reduce the diff of #11499 ## Renames All in the `Int` namespace: * `ofNat_eq_cast` → `ofNat_eq_natCast` * `cast_eq_cast_iff_Nat` → `natCast_inj` * `natCast_eq_ofNat` → `ofNat_eq_natCast` * `coe_nat_sub` → `natCast_sub` * `coe_nat_nonneg` → `natCast_nonneg` * `sign_coe_add_one` → `sign_natCast_add_one` * `nat_succ_eq_int_succ` → `natCast_succ` * `succ_neg_nat_succ` → `succ_neg_natCast_succ` * `coe_pred_of_pos` → `natCast_pred_of_pos` * `coe_nat_div` → `natCast_div` * `coe_nat_ediv` → `natCast_ediv` * `sign_coe_nat_of_nonzero` → `sign_natCast_of_ne_zero` * `toNat_coe_nat` → `toNat_natCast` * `toNat_coe_nat_add_one` → `toNat_natCast_add_one` * `coe_nat_dvd` → `natCast_dvd_natCast` * `coe_nat_dvd_left` → `natCast_dvd` * `coe_nat_dvd_right` → `dvd_natCast` * `le_coe_nat_sub` → `le_natCast_sub` * `succ_coe_nat_pos` → `succ_natCast_pos` * `coe_nat_modEq_iff` → `natCast_modEq_iff` * `coe_natAbs` → `natCast_natAbs` * `coe_nat_eq_zero` → `natCast_eq_zero` * `coe_nat_ne_zero` → `natCast_ne_zero` * `coe_nat_ne_zero_iff_pos` → `natCast_ne_zero_iff_pos` * `abs_coe_nat` → `abs_natCast` * `coe_nat_nonpos_iff` → `natCast_nonpos_iff` Also rename `Nat.coe_nat_dvd` to `Nat.cast_dvd_cast`

…atCast` (#11499) This is less exhaustive than its sibling #11486 because edge cases are harder to classify. No fundamental difficulty, just me being a bit fast and lazy. Reduce the diff of #11203

…tCast` (#11552) Reduce the diff of #11499

Reduce the diff of #11499 ## Renames All in the `Int` namespace: * `ofNat_eq_cast` → `ofNat_eq_natCast` * `cast_eq_cast_iff_Nat` → `natCast_inj` * `natCast_eq_ofNat` → `ofNat_eq_natCast` * `coe_nat_sub` → `natCast_sub` * `coe_nat_nonneg` → `natCast_nonneg` * `sign_coe_add_one` → `sign_natCast_add_one` * `nat_succ_eq_int_succ` → `natCast_succ` * `succ_neg_nat_succ` → `succ_neg_natCast_succ` * `coe_pred_of_pos` → `natCast_pred_of_pos` * `coe_nat_div` → `natCast_div` * `coe_nat_ediv` → `natCast_ediv` * `sign_coe_nat_of_nonzero` → `sign_natCast_of_ne_zero` * `toNat_coe_nat` → `toNat_natCast` * `toNat_coe_nat_add_one` → `toNat_natCast_add_one` * `coe_nat_dvd` → `natCast_dvd_natCast` * `coe_nat_dvd_left` → `natCast_dvd` * `coe_nat_dvd_right` → `dvd_natCast` * `le_coe_nat_sub` → `le_natCast_sub` * `succ_coe_nat_pos` → `succ_natCast_pos` * `coe_nat_modEq_iff` → `natCast_modEq_iff` * `coe_natAbs` → `natCast_natAbs` * `coe_nat_eq_zero` → `natCast_eq_zero` * `coe_nat_ne_zero` → `natCast_ne_zero` * `coe_nat_ne_zero_iff_pos` → `natCast_ne_zero_iff_pos` * `abs_coe_nat` → `abs_natCast` * `coe_nat_nonpos_iff` → `natCast_nonpos_iff` Also rename `Nat.coe_nat_dvd` to `Nat.cast_dvd_cast`

…atCast` (#11499) This is less exhaustive than its sibling #11486 because edge cases are harder to classify. No fundamental difficulty, just me being a bit fast and lazy. Reduce the diff of #11203

YaelDillies added awaiting-review awaiting-CI labels Mar 19, 2024

eric-wieser reviewed Mar 19, 2024

View reviewed changes

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean Outdated Show resolved Hide resolved

YaelDillies force-pushed the nat_cast_mem branch from 0afe087 to 21cfed0 Compare March 19, 2024 11:35

github-actions bot removed the awaiting-CI label Mar 19, 2024

j-loreaux approved these changes Mar 19, 2024

View reviewed changes

mattrobball reviewed Mar 19, 2024

View reviewed changes

YaelDillies added the t-algebra Algebra (groups, rings, fields etc) label Mar 20, 2024

YaelDillies mentioned this pull request Mar 20, 2024

[Merged by Bors] - feat: NNRat.cast #11203

Closed

12 tasks

eric-wieser reviewed Mar 20, 2024

View reviewed changes

Mathlib/Data/Nat/Cast/Basic.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Mar 20, 2024

View reviewed changes

Mathlib/FieldTheory/Adjoin.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Mar 20, 2024

View reviewed changes

Mathlib/FieldTheory/Subfield.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Mar 20, 2024

View reviewed changes

Mathlib/NumberTheory/LucasLehmer.lean Outdated Show resolved Hide resolved

leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. blocked-by-other-PR This PR depends on another PR to Mathlib and removed blocked-by-other-PR This PR depends on another PR to Mathlib labels Mar 20, 2024

YaelDillies added 2 commits March 20, 2024 13:31

chore: Rename coe_nat/coe_int/coe_rat to natCast/intCast/`r…

c6c391c

…atCast`

Merge remote-tracking branch 'origin/master' into nat_cast_mem

573bc54

YaelDillies force-pushed the nat_cast_mem branch from e81c896 to 573bc54 Compare March 20, 2024 13:33

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Mar 20, 2024

YaelDillies added 3 commits March 20, 2024 13:46

fix

2b644df

fix

cae3910

fix

1c1d7bb

YaelDillies added a commit that referenced this pull request Mar 20, 2024

chore: Rename cat_coe_nat/cast_coe_int to cast_natCast/`cast_in…

097ccab

…tCast` Reduce the diff of #11499

YaelDillies mentioned this pull request Mar 20, 2024

[Merged by Bors] - chore: Rename cat_coe_nat/cast_coe_int to cast_natCast/cast_intCast #11552

Closed

leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib label Mar 20, 2024

Merge remote-tracking branch 'origin/master' into nat_cast_mem

e8dfec1

leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. labels Apr 6, 2024

Merge remote-tracking branch 'origin/master' into nat_cast_mem

bdbf757

leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. labels Apr 7, 2024

Merge remote-tracking branch 'origin/master' into nat_cast_mem

163c391

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 7, 2024

github-actions bot added ready-to-merge This PR has been sent to bors. delegated and removed awaiting-review labels Apr 7, 2024

mathlib-bors bot changed the title ~~chore: Rename coe_nat/coe_int/coe_rat to natCast/intCast/ratCast~~ [Merged by Bors] - chore: Rename coe_nat/coe_int/coe_rat to natCast/intCast/ratCast Apr 7, 2024

mathlib-bors bot closed this Apr 7, 2024

mathlib-bors bot deleted the nat_cast_mem branch April 7, 2024 18:52

Louddy pushed a commit that referenced this pull request Apr 15, 2024

chore: Rename cat_coe_nat/cast_coe_int to cast_natCast/`cast_in…

0e63db4

…tCast` (#11552) Reduce the diff of #11499

atarnoam pushed a commit that referenced this pull request Apr 16, 2024

chore: Rename cat_coe_nat/cast_coe_int to cast_natCast/`cast_in…

8c9820a

…tCast` (#11552) Reduce the diff of #11499

uniwuni pushed a commit that referenced this pull request Apr 19, 2024

chore: Rename cat_coe_nat/cast_coe_int to cast_natCast/`cast_in…

80e8412

…tCast` (#11552) Reduce the diff of #11499

callesonne pushed a commit that referenced this pull request Apr 22, 2024

chore: Rename cat_coe_nat/cast_coe_int to cast_natCast/`cast_in…

457e481

…tCast` (#11552) Reduce the diff of #11499

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore: Rename `coe_nat`/`coe_int`/`coe_rat` to `natCast`/`intCast`/`ratCast` #11499

[Merged by Bors] - chore: Rename `coe_nat`/`coe_int`/`coe_rat` to `natCast`/`intCast`/`ratCast` #11499

YaelDillies commented Mar 19, 2024 •

edited by Parcly-Taxel

Loading

fpvandoorn commented Mar 19, 2024 •

edited

Loading

fpvandoorn commented Mar 19, 2024

YaelDillies commented Mar 19, 2024 •

edited

Loading

j-loreaux left a comment

eric-wieser left a comment

fpvandoorn commented Apr 7, 2024

mathlib-bors bot commented Apr 7, 2024

mathlib-bors bot commented Apr 7, 2024

[Merged by Bors] - chore: Rename coe_nat/coe_int/coe_rat to natCast/intCast/ratCast #11499

[Merged by Bors] - chore: Rename coe_nat/coe_int/coe_rat to natCast/intCast/ratCast #11499

Conversation

YaelDillies commented Mar 19, 2024 • edited by Parcly-Taxel Loading

fpvandoorn commented Mar 19, 2024 • edited Loading

fpvandoorn commented Mar 19, 2024

YaelDillies commented Mar 19, 2024 • edited Loading

j-loreaux left a comment

Choose a reason for hiding this comment

eric-wieser left a comment

Choose a reason for hiding this comment

fpvandoorn commented Apr 7, 2024

mathlib-bors bot commented Apr 7, 2024

mathlib-bors bot commented Apr 7, 2024

[Merged by Bors] - chore: Rename `coe_nat`/`coe_int`/`coe_rat` to `natCast`/`intCast`/`ratCast` #11499

[Merged by Bors] - chore: Rename `coe_nat`/`coe_int`/`coe_rat` to `natCast`/`intCast`/`ratCast` #11499

YaelDillies commented Mar 19, 2024 •

edited by Parcly-Taxel

Loading

fpvandoorn commented Mar 19, 2024 •

edited

Loading

YaelDillies commented Mar 19, 2024 •

edited

Loading