[Merged by Bors] - chore(algebra/group/type_tags): add `additive.to_mul` etc #2363

urkud · 2020-04-08T20:26:38Z

Don't make additive and multiplicative irreducible (yet?) because
it breaks compilation here and there.

Also prove that homomorphisms from ℕ, ℤ and their multiplicative
versions are defined by the image of 1.

TO CONTRIBUTORS:

Make sure you have:

reviewed and applied the coding style: coding, naming
reviewed and applied the documentation requirements
for tactics:
- added or adapted documentation in the tactic doc entries
- write an example of use of the new feature in test/tactics.lean or another test file
make sure definitions and lemmas are put in the right files
make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

Don't make `additive` and `multiplicative` irreducible (yet?) because it breaks compilation here and there. Also prove that homomorphisms from `ℕ`, `ℤ` and their `multiplicative` versionsare defined by the image of `1`.

urkud · 2020-04-08T20:28:31Z

@gebner @digama0 This is supposed to be a version of #2292 that allows us to visually tell * in multiplicative nat from * in nat while not breaking existing code.

gebner · 2020-04-09T13:40:49Z

src/algebra/group/type_tags.lean

+rfl
+
+@[simp] lemma to_add_mul [has_add α] (x y : multiplicative α) :
+  (x * y).to_add = x.to_add + y.to_add :=


@robertylewis Can we hook this up to norm_cast even though it's not (and should not be) coe?

Not really. It might work with the current norm_cast, but in the open PR (that will be finished eventually), we classify lemmas according to the position of coe. It's not really designed to work with arbitrary coercion operators.

gebner · 2020-04-09T13:43:40Z

src/algebra/group_power.lean

@@ -647,3 +649,41 @@ end int

 @[simp] lemma neg_square {α} [ring α] (z : α) : (-z)^2 = z^2 :=
 by simp [pow, monoid.pow]
+
+@[simp] lemma pow_of_add [add_monoid A] (x : A) (n : ℕ) :
+  (multiplicative.of_add x)^n = multiplicative.of_add (n • x) := rfl


Most of the time the simp-lemmas go the other way, that is, they move the of_add into the operation. I don't know which direction is best.

Oh, I missed this comment before. Yes, this definitely goes against the grain of the usual simp normal form.

You can think that you move of_add outside or pow inside. I'm not sure which point of view is more appropriate here. In all my use cases I want to rewrite this lemma left to right but it's OK with me to remove it from simp completely and use simp [pow_of_add].

OTOH, I move to_add inside of * in another lemma. I'll see if rewriting in the other direction closes the goals.

src/algebra/group/type_tags.lean

gebner · 2020-04-18T12:23:23Z

I've changed the pow_of_add and gpow_of_add into the commonly used direction.

bors r+

bors · 2020-04-18T12:23:25Z

👎 Rejected by label

gebner · 2020-04-18T12:23:37Z

Ooops.

bors r+

Don't make `additive` and `multiplicative` irreducible (yet?) because it breaks compilation here and there. Also prove that homomorphisms from `ℕ`, `ℤ` and their `multiplicative` versions are defined by the image of `1`. Co-authored-by: Gabriel Ebner <gebner@gebner.org>

bors · 2020-04-18T15:15:10Z

Pull request successfully merged into master.

Build succeeded:

Build mathlib

Also add an explicit instance for `submodule.has_coe_to_sort`. This way `rintro ⟨x, hx⟩` results in `(hx : x ∈ p)`. Also fixes some timeouts introduced by #2363. See Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/partrec_code

…-community#2363) Don't make `additive` and `multiplicative` irreducible (yet?) because it breaks compilation here and there. Also prove that homomorphisms from `ℕ`, `ℤ` and their `multiplicative` versions are defined by the image of `1`. Co-authored-by: Gabriel Ebner <gebner@gebner.org>

Also add an explicit instance for `submodule.has_coe_to_sort`. This way `rintro ⟨x, hx⟩` results in `(hx : x ∈ p)`. Also fixes some timeouts introduced by leanprover-community#2363. See Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/partrec_code

…-community#2363) Don't make `additive` and `multiplicative` irreducible (yet?) because it breaks compilation here and there. Also prove that homomorphisms from `ℕ`, `ℤ` and their `multiplicative` versions are defined by the image of `1`. Co-authored-by: Gabriel Ebner <gebner@gebner.org>

Also add an explicit instance for `submodule.has_coe_to_sort`. This way `rintro ⟨x, hx⟩` results in `(hx : x ∈ p)`. Also fixes some timeouts introduced by leanprover-community#2363. See Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/partrec_code

…-community#2363) Don't make `additive` and `multiplicative` irreducible (yet?) because it breaks compilation here and there. Also prove that homomorphisms from `ℕ`, `ℤ` and their `multiplicative` versions are defined by the image of `1`. Co-authored-by: Gabriel Ebner <gebner@gebner.org>

Also add an explicit instance for `submodule.has_coe_to_sort`. This way `rintro ⟨x, hx⟩` results in `(hx : x ∈ p)`. Also fixes some timeouts introduced by leanprover-community#2363. See Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/partrec_code

urkud added 2 commits April 8, 2020 15:45

chore(algebra/group/type_tags): add additive.to_mul etc

68404ee

Don't make `additive` and `multiplicative` irreducible (yet?) because it breaks compilation here and there. Also prove that homomorphisms from `ℕ`, `ℤ` and their `multiplicative` versionsare defined by the image of `1`.

Rename, use in submonoid

99df619

urkud added the awaiting-review The author would like community review of the PR label Apr 8, 2020

jcommelin requested review from gebner and digama0 April 9, 2020 13:15

gebner approved these changes Apr 9, 2020

View reviewed changes

urkud added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Apr 9, 2020

urkud commented Apr 9, 2020

View reviewed changes

src/algebra/group/type_tags.lean Outdated Show resolved Hide resolved

urkud commented Apr 9, 2020

View reviewed changes

src/algebra/group/type_tags.lean Outdated Show resolved Hide resolved

Fix typos in names

1564721

jcommelin assigned gebner Apr 10, 2020

gebner added 2 commits April 18, 2020 11:36

Reverse pow_of_add and gpow_of_add simp lemmas.

a00ab78

Merge remote-tracking branch 'origin/master' into multiplicative-to-of

c8bc160

gebner removed the awaiting-author A reviewer has asked the author a question or requested changes label Apr 18, 2020

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Apr 18, 2020

bors bot changed the title ~~chore(algebra/group/type_tags): add additive.to_mul etc~~ [Merged by Bors] - chore(algebra/group/type_tags): add additive.to_mul etc Apr 18, 2020

bors bot closed this Apr 18, 2020

bors bot deleted the multiplicative-to-of branch April 18, 2020 15:15

urkud mentioned this pull request May 1, 2020

[Merged by Bors] - feat(*): several @[simp] lemmas #2579

Closed

bryangingechen mentioned this pull request May 1, 2020

[Merged by Bors] - fix(data/int/basic): use has_coe_t to prevent looping #2573

Closed

eric-wieser mentioned this pull request Oct 5, 2020

refactor(algebra/group): make multiplicative and additive irreducible #2292

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore(algebra/group/type_tags): add `additive.to_mul` etc #2363

[Merged by Bors] - chore(algebra/group/type_tags): add `additive.to_mul` etc #2363

urkud commented Apr 8, 2020

urkud commented Apr 8, 2020

gebner Apr 9, 2020

robertylewis Apr 9, 2020

gebner Apr 9, 2020

robertylewis Apr 9, 2020

urkud Apr 9, 2020

urkud Apr 9, 2020

gebner commented Apr 18, 2020

bors bot commented Apr 18, 2020

gebner commented Apr 18, 2020

bors bot commented Apr 18, 2020

[Merged by Bors] - chore(algebra/group/type_tags): add additive.to_mul etc #2363

[Merged by Bors] - chore(algebra/group/type_tags): add additive.to_mul etc #2363

Conversation

urkud commented Apr 8, 2020

urkud commented Apr 8, 2020

gebner Apr 9, 2020

Choose a reason for hiding this comment

robertylewis Apr 9, 2020

Choose a reason for hiding this comment

gebner Apr 9, 2020

Choose a reason for hiding this comment

robertylewis Apr 9, 2020

Choose a reason for hiding this comment

urkud Apr 9, 2020

Choose a reason for hiding this comment

urkud Apr 9, 2020

Choose a reason for hiding this comment

gebner commented Apr 18, 2020

bors bot commented Apr 18, 2020

gebner commented Apr 18, 2020

bors bot commented Apr 18, 2020

[Merged by Bors] - chore(algebra/group/type_tags): add `additive.to_mul` etc #2363

[Merged by Bors] - chore(algebra/group/type_tags): add `additive.to_mul` etc #2363