Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: missing lemmas about Finsupp.update #9316

Closed
wants to merge 7 commits into from
Closed

[Merged by Bors] - feat: missing lemmas about Finsupp.update #9316

Changes from 3 commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
8befdb8
feat: missing lemmas about `Finsupp.update`
eric-wieser Dec 28, 2023
c14eb3c
stupid whitespace
eric-wieser Dec 28, 2023
99dd110
stupid whitespace
eric-wieser Dec 28, 2023
f587233
Update Defs.lean
eric-wieser Dec 28, 2023
21b454e
Update Mathlib/Data/Finsupp/Defs.lean
eric-wieser Dec 30, 2023
3b170ee
one more lemma
eric-wieser Jan 1, 2024
a76be2d
Yael's comments
eric-wieser Jan 1, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 21 additions & 0 deletions Mathlib/Data/Finsupp/Defs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -600,6 +600,11 @@
congr; apply Subsingleton.elim
#align finsupp.support_update_ne_zero Finsupp.support_update_ne_zero

@[simp] theorem update_idem (f : α →₀ M) (a : α) (b c : M) :
eric-wieser marked this conversation as resolved.
Show resolved Hide resolved
update (update f a b) a c = update f a c :=
letI := Classical.decEq α
FunLike.coe_injective <| Function.update_idem _ _ _

end Update

/-! ### Declarations about `erase` -/
Expand Down Expand Up @@ -673,6 +678,22 @@
classical rw [← support_eq_empty, support_erase, support_zero, erase_empty]
#align finsupp.erase_zero Finsupp.erase_zero

theorem update_eq_erase (f : α →₀ M) (a : α) : update f a 0 = f.erase a :=
Copy link
Collaborator

Choose a reason for hiding this comment

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

wouldn't the name update_zero_eq_erase be more explicit?

Copy link
Member Author

Choose a reason for hiding this comment

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

Or perhaps erase_eq_update(_zero) after flipping the direction?

Copy link
Collaborator

Choose a reason for hiding this comment

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

Yes. For a surprising reason, the absence of zero doesn't disturb me in the other direction.

Copy link
Member Author

Choose a reason for hiding this comment

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

I've gone for reversing it then

letI := Classical.decEq α
ext fun _ => Function.update_apply _ _ _ _

@[simp] theorem erase_idem (f : α →₀ M) (a : α) :

Check failure on line 685 in Mathlib/Data/Finsupp/Defs.lean

View workflow job for this annotation

GitHub Actions / Build 

Finsupp.erase_idem.{u_5, u_1} simp can prove this:
eric-wieser marked this conversation as resolved.
Show resolved Hide resolved
erase a (erase a f) = erase a f := by
rw [← update_eq_erase, ← update_eq_erase, update_idem]

@[simp] theorem update_erase (f : α →₀ M) (a : α) (b : M) :
update (erase a f) a b = update f a b := by
eric-wieser marked this conversation as resolved.
Show resolved Hide resolved
rw [← update_eq_erase, update_idem]

@[simp] theorem erase_update (f : α →₀ M) (a : α) (b : M) :
erase a (update f a b) = erase a f := by
Copy link
Collaborator

Choose a reason for hiding this comment

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

Suggested change
@[simp] theorem erase_update (f : α →₀ M) (a : α) (b : M) :
erase a (update f a b) = erase a f := by
@[simp] theorem erase_update_self (f : α →₀ M) (a : α) (b : M) :
erase a (update f a b) = erase a f := by

Copy link
Member Author

@eric-wieser eric-wieser Jan 1, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

On Finset this is called erase_insert_eq_erase; shall I change to erase_update_eq_erase?

rw [← update_eq_erase, ← update_eq_erase, update_idem]

end Erase

/-! ### Declarations about `onFinset` -/
Expand Down
Loading