feat(Data/Nat/Choose): add `Choose.lucas`

[grhkm21]

trafficstars

TODO: Name the stuff properly and finish the proofs. Suggestions on naming would be greatly appreciated.

[kim-em]

Please fix the long lines the linter is complaining about.

[kim-em]

(You can change the label back to awaiting-review when you're ready!)

[grhkm21]

Sorry for the long wait, exams :( Fixed the issues above!

[github-actions[bot]]

PR summary e82d217ef5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Data.Nat.Choose.Lucas	1107

---

Declarations diff

+ add_pow_eq_add_pow_mod_mul_pow_add_pow_div + choose_modEq_choose_mod_mul_choose_div + choose_modEq_choose_mod_mul_choose_div_nat + choose_modEq_choose_mul_prod_range_choose + choose_modEq_prod_range_choose + choose_modEq_prod_range_choose_nat + lucas_theorem + lucas_theorem_nat + sub_pow_eq_sub_pow_mod_mul_pow_sub_pow_div

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[grhkm21]

I have reverted the ite -> if-then-else changes (TIL about git reset --patch). Hope it's okay now :D

[grhkm21]

Okay I should have cleaned up stuff. Also I realised a proof didn't even compile, so I fixed that (it depended on the prod_ite_eq_iff thing

[grhkm21]

Sorry, my browser automatically corrects wikipedia links to wikiwand.

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[jcommelin]

I take it that the TODO in the PR commit message (i.e. the top post above) no longer applies? If so, please update it.

[grhkm21]

@jcommelin Done, sorry about that

[kim-em]

bors d+

[mathlib-bors[bot]]

:v: grhkm21 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[grhkm21]

@b-mehta do you mind reviewing the latest (two) commits? I added the nat versions as suggested

[Ruben-VandeVelde]

Looks like you got hit by the new linter:

warning: ././././Mathlib/Data/Nat/Choose/Lucas.lean:99:0: unclosed sections or namespaces; expected: '

end Choose'

[jcommelin]

Thanks a lot for this contribution! Let's just merge this. Follow-up versions can be done in a follow-up PR.

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style