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

eric-wieser · 2023-12-28T15:46:58Z

Mathlib/Data/Finsupp/Defs.lean

AntoineChambert-Loir · 2023-12-28T16:24:50Z

Mathlib/Data/Finsupp/Defs.lean

@@ -673,6 +678,22 @@ theorem erase_zero (a : α) : erase a (0 : α →₀ M) = 0 := by
  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 :=


wouldn't the name update_zero_eq_erase be more explicit?

Or perhaps erase_eq_update(_zero) after flipping the direction?

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

I've gone for reversing it then

Mathlib/Data/Finsupp/Defs.lean

AntoineChambert-Loir · 2023-12-29T21:43:16Z

CI/Build fails at Mathlib/Data/Finsupp/Defs.lean:685:9:
error: Finsupp.erase_idem.{u_5, u_1} simp can prove this
I don't how how to fix that except by removing the @[simp] tag before the function.

Mathlib/Data/Finsupp/Defs.lean

jcommelin · 2024-01-01T18:48:05Z

Thanks 🎉

bors merge

YaelDillies · 2024-01-01T18:49:27Z

Mathlib/Data/Finsupp/Defs.lean

@@ -673,6 +678,23 @@ theorem erase_zero (a : α) : erase a (0 : α →₀ M) = 0 := by
  classical rw [← support_eq_empty, support_erase, support_zero, erase_empty]
 #align finsupp.erase_zero Finsupp.erase_zero

+theorem erase_eq_update (f : α →₀ M) (a : α) : f.erase a = update f a 0 :=


Suggested change

theorem erase_eq_update (f : α →₀ M) (a : α) : f.erase a = update f a 0 :=

theorem erase_eq_update_zero (f : α →₀ M) (a : α) : f.erase a = update f a 0 :=

for discoverability. I would even consider

Suggested change

theorem erase_eq_update (f : α →₀ M) (a : α) : f.erase a = update f a 0 :=

@[simp]

theorem update_zero_eq_erase (f : α →₀ M) (a : α) : f.erase a = update f a 0 :=

Did you mean to flip the direction in that last one?

Note that there was already discussion about this in #9316 (comment)

Yep, sorry, I meant it flipped

Mathlib/Data/Finsupp/Defs.lean

YaelDillies · 2024-01-01T18:51:03Z

Mathlib/Data/Finsupp/Defs.lean

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


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

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

eric-wieser · 2024-01-01T18:52:08Z

bors r-

mathlib-bors · 2024-01-01T18:52:11Z

Canceled.

YaelDillies · 2024-01-01T20:50:53Z

I think you should

add update_erase : update (erase a f) a (f a) = f
reverse erase_eq_update_zero to update_zero_eq_erase

Then I'm happy.

YaelDillies · 2024-01-01T20:58:46Z

I have been convinced otherwise in DMs.

maintainer merge

github-actions · 2024-01-01T20:59:00Z

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

eric-wieser · 2024-01-01T22:18:22Z

bors merge

mathlib-bors · 2024-01-02T00:04:20Z

Pull request successfully merged into master.

Build succeeded!

And happy new year! 🎉

feat: missing lemmas about Finsupp.update

8befdb8

eric-wieser added awaiting-review The author would like community review of the PR awaiting-CI labels Dec 28, 2023

github-actions bot reviewed Dec 28, 2023

View reviewed changes

Mathlib/Data/Finsupp/Defs.lean Outdated Show resolved Hide resolved

Mathlib/Data/Finsupp/Defs.lean Outdated Show resolved Hide resolved

eric-wieser mentioned this pull request Dec 28, 2023

[Merged by Bors] - feat: add Finset.piAntidiagonal #7904

Closed

1 task

stupid whitespace

c14eb3c

github-actions bot reviewed Dec 28, 2023

View reviewed changes

Mathlib/Data/Finsupp/Defs.lean Outdated Show resolved Hide resolved

stupid whitespace

99dd110

eric-wieser added the easy < 20s of review time. See the lifecycle page for guidelines. label Dec 28, 2023

AntoineChambert-Loir reviewed Dec 28, 2023

View reviewed changes

Mathlib/Data/Finsupp/Defs.lean Show resolved Hide resolved

Update Defs.lean

f587233

eric-wieser commented Dec 30, 2023

View reviewed changes

Mathlib/Data/Finsupp/Defs.lean Outdated Show resolved Hide resolved

Update Mathlib/Data/Finsupp/Defs.lean

21b454e

github-actions bot removed the awaiting-CI label Dec 30, 2023

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Jan 1, 2024

YaelDillies reviewed Jan 1, 2024

View reviewed changes

one more lemma

3b170ee

YaelDillies added awaiting-author A reviewer has asked the author a question or requested changes and removed ready-to-merge This PR has been sent to bors. labels Jan 1, 2024

Yael's comments

a76be2d

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jan 1, 2024

mathlib-bors bot pushed a commit that referenced this pull request Jan 1, 2024

feat: missing lemmas about Finsupp.update (#9316)

2a17457

mathlib-bors bot changed the title ~~feat: missing lemmas about Finsupp.update~~ [Merged by Bors] - feat: missing lemmas about Finsupp.update Jan 2, 2024

mathlib-bors bot closed this Jan 2, 2024

mathlib-bors bot deleted the eric-wieser/finsupp-update-lemmas branch January 2, 2024 00:04

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

eric-wieser commented Dec 28, 2023

AntoineChambert-Loir Dec 28, 2023

eric-wieser Dec 28, 2023

AntoineChambert-Loir Dec 28, 2023

eric-wieser Dec 28, 2023

AntoineChambert-Loir commented Dec 29, 2023

jcommelin commented Jan 1, 2024

YaelDillies Jan 1, 2024

eric-wieser Jan 1, 2024

eric-wieser Jan 1, 2024

YaelDillies Jan 1, 2024

YaelDillies Jan 1, 2024

eric-wieser Jan 1, 2024 •

edited

Loading

eric-wieser commented Jan 1, 2024

mathlib-bors bot commented Jan 1, 2024

YaelDillies commented Jan 1, 2024

YaelDillies commented Jan 1, 2024

github-actions bot commented Jan 1, 2024

eric-wieser commented Jan 1, 2024

mathlib-bors bot commented Jan 2, 2024

	theorem erase_eq_update (f : α →₀ M) (a : α) : f.erase a = update f a 0 :=
	theorem erase_eq_update_zero (f : α →₀ M) (a : α) : f.erase a = update f a 0 :=

	theorem erase_eq_update (f : α →₀ M) (a : α) : f.erase a = update f a 0 :=
	@[simp]
	theorem update_zero_eq_erase (f : α →₀ M) (a : α) : f.erase a = update f a 0 :=

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

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

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

Conversation

eric-wieser commented Dec 28, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

AntoineChambert-Loir commented Dec 29, 2023

jcommelin commented Jan 1, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eric-wieser Jan 1, 2024 • edited Loading

Choose a reason for hiding this comment

eric-wieser commented Jan 1, 2024

mathlib-bors bot commented Jan 1, 2024

YaelDillies commented Jan 1, 2024

YaelDillies commented Jan 1, 2024

github-actions bot commented Jan 1, 2024

eric-wieser commented Jan 1, 2024

mathlib-bors bot commented Jan 2, 2024

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

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

eric-wieser Jan 1, 2024 •

edited

Loading