[Merged by Bors] - Composing non_zero function with injective fun is non_zero by CBirkbeck · Pull Request #11244 · leanprover-community/mathlib4

CBirkbeck · 2024-03-08T15:58:48Z

Some basic missing lemmas about injective function composition. See this Zulip thread

adomani

Thanks!

Mathlib/Algebra/Group/Pi/Basic.lean

Co-authored-by: damiano <adomani@gmail.com>

adomani

Sorry, I noticed these after my previous review!

Mathlib/Algebra/Group/Pi/Basic.lean

Co-authored-by: damiano <adomani@gmail.com>

Mathlib/Algebra/Group/Pi/Basic.lean

Co-authored-by: damiano <adomani@gmail.com>

adomani

This is surely the most corrections that I have suggested on any single line of code! 😄

Mathlib/Algebra/Group/Pi/Basic.lean

CBirkbeck · 2024-03-08T21:46:53Z

This is surely the most corrections that I have suggested on any single line of code! 😄

Hahaha I'm sorry! I really didn't look at it very closely since most of it was written by people that know more than me!

Co-authored-by: damiano <adomani@gmail.com>

CBirkbeck · 2024-03-12T11:42:38Z

Ok this should be ready to go I think.

mattrobball · 2024-03-12T23:19:15Z

Thanks!

bors merge

Mathlib/Algebra/Group/Pi/Basic.lean

Some basic missing lemmas about injective function composition. See this Zulip [thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/injective.20function.20composed.20with.20non.20zero.20function.20ne.20zero) Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>

eric-wieser · 2024-03-12T23:35:28Z

bors r-

mathlib-bors · 2024-03-12T23:35:30Z

Canceled.

eric-wieser · 2024-03-12T23:43:42Z

I don't think there is ever a reason to write OfNat T 0 in mathlib over Zero T; and once you use the latter, to_additive works!

I pushed a change to that effect; please merge if you're happy with it

bors d+

mathlib-bors · 2024-03-12T23:43:47Z

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

CBirkbeck · 2024-03-13T13:54:26Z

bors r+

Some basic missing lemmas about injective function composition. See this Zulip [thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/injective.20function.20composed.20with.20non.20zero.20function.20ne.20zero) Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

CBirkbeck · 2024-03-13T13:55:52Z

I don't think there is ever a reason to write OfNat T 0 in mathlib over Zero T; and once you use the latter, to_additive works!

I pushed a change to that effect; please merge if you're happy with it

Ah yes much better! I had only used OfNat as it was the minimal think it was asking to state and prove the lemmas. But Zero T is definitely better.

mathlib-bors · 2024-03-13T15:01:57Z

Pull request successfully merged into master.

Build succeeded:

YaelDillies · 2024-03-18T21:35:26Z

Mathlib/Algebra/Group/Pi/Basic.lean

+    g ∘ f = Function.const _ (g b) ↔ f = Function.const _ b :=
+  hg.comp_left.eq_iff' rfl


Suggested change

g ∘ f = Function.const _ (g b) ↔ f = Function.const _ b :=

hg.comp_left.eq_iff' rfl

g ∘ f = const _ (g b) ↔ f = const _ b := hg.comp_left.eq_iff

I don't know what to do about these comments, now that its been merged? make a new pr?

Yeah that would be great, thank you!

YaelDillies · 2024-03-18T21:35:58Z

Mathlib/Algebra/Group/Pi/Basic.lean

  ⟨injective_pi_map fun i => (hF i).injective, surjective_pi_map fun i => (hF i).surjective⟩
 #align function.bijective_pi_map Function.bijective_pi_map

+lemma comp_eq_const_iff (b : β) (f : α → β) {g : β → γ} (hg : Injective g) :


Suggested change

lemma comp_eq_const_iff (b : β) (f : α → β) {g : β → γ} (hg : Injective g) :

lemma comp_eq_const {b : β} {f : α → β} {g : β → γ} (hg : Injective g) :

Same below

YaelDillies · 2024-03-18T21:36:36Z

Mathlib/Algebra/Group/Pi/Basic.lean

+  hg.comp_left.eq_iff' rfl
+
+@[to_additive]
+lemma comp_eq_one_iff [One β] [One γ] (f : α → β) {g : β → γ} (hg : Injective g) (hg0 : g 1 = 1) :


hg0 is a weird assumption name for something talking about 1

Ah its because it was a zero to start and then Eric saw that it would work more generally with a to_additive and I didn't think to change the name after.

Some basic missing lemmas about injective function composition. See this Zulip [thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/injective.20function.20composed.20with.20non.20zero.20function.20ne.20zero) Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

We show that Eisenstein Series are MDifferentiable - [x] depends on: #10377 - [x] depends on: #11244 Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>

composing non_zero function with inj fun is non_zero

3600a74

CBirkbeck mentioned this pull request Mar 8, 2024

[Merged by Bors] - Eisenstein series are mdifferentiable #11013

Closed

2 tasks

CBirkbeck added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Mar 8, 2024

CBirkbeck requested a review from eric-wieser March 8, 2024 16:08

CBirkbeck mentioned this pull request Mar 8, 2024

[Merged by Bors] - Eisenstein series uniform convergence #10377

Closed

5 tasks

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Mar 8, 2024

adomani approved these changes Mar 8, 2024

View reviewed changes

Mathlib/Algebra/Group/Pi/Basic.lean Outdated Show resolved Hide resolved

Mathlib/Algebra/Group/Pi/Basic.lean Outdated Show resolved Hide resolved

Mathlib/Algebra/Group/Pi/Basic.lean Outdated Show resolved Hide resolved

adomani added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Mar 8, 2024

CBirkbeck and others added 3 commits March 8, 2024 18:46

Update Mathlib/Algebra/Group/Pi/Basic.lean

e5be53b

Co-authored-by: damiano <adomani@gmail.com>

Update Mathlib/Algebra/Group/Pi/Basic.lean

5441068

Co-authored-by: damiano <adomani@gmail.com>

Update Mathlib/Algebra/Group/Pi/Basic.lean

d2adff3

Co-authored-by: damiano <adomani@gmail.com>

adomani reviewed Mar 8, 2024

View reviewed changes

CBirkbeck and others added 4 commits March 8, 2024 19:04

Update Mathlib/Algebra/Group/Pi/Basic.lean

a6b08f2

Co-authored-by: damiano <adomani@gmail.com>

Update Mathlib/Algebra/Group/Pi/Basic.lean

6b0035f

Co-authored-by: damiano <adomani@gmail.com>

Update Mathlib/Algebra/Group/Pi/Basic.lean

c3a2e31

Co-authored-by: damiano <adomani@gmail.com>

Update Mathlib/Algebra/Group/Pi/Basic.lean

e62adaf

Co-authored-by: damiano <adomani@gmail.com>

adomani reviewed Mar 8, 2024

View reviewed changes

Mathlib/Algebra/Group/Pi/Basic.lean Outdated Show resolved Hide resolved

Update Mathlib/Algebra/Group/Pi/Basic.lean

1a94fb0

Co-authored-by: damiano <adomani@gmail.com>

adomani reviewed Mar 8, 2024

View reviewed changes

Mathlib/Algebra/Group/Pi/Basic.lean Outdated Show resolved Hide resolved

Mathlib/Algebra/Group/Pi/Basic.lean Outdated Show resolved Hide resolved

CBirkbeck and others added 2 commits March 12, 2024 09:56

Update Mathlib/Algebra/Group/Pi/Basic.lean

674b696

Co-authored-by: damiano <adomani@gmail.com>

Update Mathlib/Algebra/Group/Pi/Basic.lean

cab9ccc

Co-authored-by: damiano <adomani@gmail.com>

CBirkbeck added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Mar 12, 2024

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Mar 12, 2024

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

tb65536 reviewed Mar 12, 2024

View reviewed changes

Mathlib/Algebra/Group/Pi/Basic.lean Outdated Show resolved Hide resolved

to_additive

d4b2753

github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Mar 12, 2024

line wrap

851abb8

mathlib-bors bot changed the title ~~Composing non_zero function with injective fun is non_zero~~ [Merged by Bors] - Composing non_zero function with injective fun is non_zero Mar 13, 2024

mathlib-bors bot closed this Mar 13, 2024

mathlib-bors bot deleted the injective_fun_comp_lemmas branch March 13, 2024 15:02

YaelDillies reviewed Mar 18, 2024

View reviewed changes

grunweg added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Mar 25, 2024

mathlib-bors bot pushed a commit that referenced this pull request May 27, 2024

Eisenstein series are mdifferentiable (#11013)

3efcf49

We show that Eisenstein Series are MDifferentiable - [x] depends on: #10377 - [x] depends on: #11244 Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>

callesonne pushed a commit that referenced this pull request Jun 4, 2024

Eisenstein series are mdifferentiable (#11013)

f193746

We show that Eisenstein Series are MDifferentiable - [x] depends on: #10377 - [x] depends on: #11244 Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>

js2357 pushed a commit that referenced this pull request Jun 18, 2024

Eisenstein series are mdifferentiable (#11013)

fc93e2f

We show that Eisenstein Series are MDifferentiable - [x] depends on: #10377 - [x] depends on: #11244 Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>

		g ∘ f = Function.const _ (g b) ↔ f = Function.const _ b :=
		hg.comp_left.eq_iff' rfl

	g ∘ f = Function.const _ (g b) ↔ f = Function.const _ b :=
	hg.comp_left.eq_iff' rfl
	g ∘ f = const _ (g b) ↔ f = const _ b := hg.comp_left.eq_iff

	lemma comp_eq_const_iff (b : β) (f : α → β) {g : β → γ} (hg : Injective g) :
	lemma comp_eq_const {b : β} {f : α → β} {g : β → γ} (hg : Injective g) :

Conversation

CBirkbeck commented Mar 8, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

adomani left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

adomani left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

adomani left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

CBirkbeck commented Mar 8, 2024

Uh oh!

CBirkbeck commented Mar 12, 2024

Uh oh!

mattrobball commented Mar 12, 2024

Uh oh!

Uh oh!

eric-wieser commented Mar 12, 2024

Uh oh!

mathlib-bors bot commented Mar 12, 2024

Uh oh!

eric-wieser commented Mar 12, 2024

Uh oh!

mathlib-bors bot commented Mar 12, 2024

Uh oh!

CBirkbeck commented Mar 13, 2024

Uh oh!

CBirkbeck commented Mar 13, 2024

Uh oh!

mathlib-bors bot commented Mar 13, 2024

Uh oh!

YaelDillies Mar 18, 2024

Choose a reason for hiding this comment

Uh oh!

CBirkbeck Mar 19, 2024

Choose a reason for hiding this comment

Uh oh!

YaelDillies Mar 19, 2024

Choose a reason for hiding this comment

Uh oh!

YaelDillies Mar 18, 2024

Choose a reason for hiding this comment

Uh oh!

YaelDillies Mar 18, 2024

Choose a reason for hiding this comment

Uh oh!

CBirkbeck Mar 19, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

CBirkbeck commented Mar 8, 2024 •

edited

Loading

CBirkbeck Mar 19, 2024 •

edited

Loading