chore(Data/Finset/Card): rename pred_card_le_card_erase to sub_one_card_le_card_erase#36832
chore(Data/Finset/Card): rename pred_card_le_card_erase to sub_one_card_le_card_erase#36832KryptosAI wants to merge 4 commits intoleanprover-community:masterfrom
pred_card_le_card_erase to sub_one_card_le_card_erase#36832Conversation
…_card_le_card_erase` The name `pred_card_le_card_erase` suggests `Nat.pred` but the statement uses `- 1` (i.e., `Nat.sub 1`). Rename to `sub_one_card_le_card_erase` to match the actual statement. A deprecated alias is added for backwards compatibility. Updates downstream references in Powerset.lean, SubsetSum.lean, and EraseLead.lean. Addresses part of leanprover-community#21584.
github-actions
bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary 6ef8cc2731Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
Co-Authored-By: Claude Opus 4.6 (1M context) <[email protected]>
Multramate
left a comment
Multramate
left a comment
There was a problem hiding this comment.
Could you also do this change for card_eq_succ and card_eq_succ_iff_cons? Thanks!
| Multiset.card_erase_le | ||
|
|
||
| theorem pred_card_le_card_erase : #s - 1 ≤ #(s.erase a) := by grind | ||
| theorem sub_one_card_le_card_erase : #s - 1 ≤ #(s.erase a) := by grind |
There was a problem hiding this comment.
| theorem sub_one_card_le_card_erase : #s - 1 ≤ #(s.erase a) := by grind | |
| theorem card_sub_one_le_card_erase : #s - 1 ≤ #(s.erase a) := by grind |
There was a problem hiding this comment.
Applied in 0d4ae07. I renamed this to card_sub_one_le_card_erase, and I left deprecated aliases for both pred_card_le_card_erase and sub_one_card_le_card_erase.
|
Also addressed the consistency suggestion from the approved review in 0d4ae07: |
3 participants
Summary
The name
pred_card_le_card_erasesuggestsNat.predbut the statement uses- 1(i.e.,Nat.sub 1). Rename tosub_one_card_le_card_eraseto match the actual statement.A deprecated alias is added for backwards compatibility.
Files changed
Mathlib/Data/Finset/Card.lean— definition renamed + deprecated aliasMathlib/Data/Finset/Powerset.lean— reference updatedMathlib/Combinatorics/Additive/SubsetSum.lean— reference updatedMathlib/Algebra/Polynomial/EraseLead.lean— reference updatedAddresses the
Finset.pred_card_le_card_eraseitem in #21584.AI disclosure
I used Claude Code to explore the codebase (finding all references to rename) and to draft the PR description. I reviewed and understand all changes — these are straightforward renames with a deprecated alias.