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(group_theory/subgroup): add mem_map_of_mem #7459

Closed

riccardobrasca wants to merge 16 commits into master from mem_map_of_mem

Member

riccardobrasca commented May 4, 2021 •

edited

From LTE.

Written by @PatrickMassot


          feat(group_theory/subgroup): add mem_map_of_mem

riccardobrasca added the awaiting-review label

eric-wieser reviewed

View reviewed changes

src/group_theory/subgroup.lean Outdated Show resolved Hide resolved


          Update src/group_theory/subgroup.lean

31501ad

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

eric-wieser reviewed

View reviewed changes

src/group_theory/subgroup.lean Outdated Show resolved Hide resolved


          add mem_map_of_mem'

dadc083

Member

eric-wieser commented May 4, 2021

Oh, it turns out that submodule.mem_map_of_mem uses the mem version after all. So maybe the way forward is:

Make the submonoid version match the submodule version (and your original version), by renaming mem_map_of_mem' back to mem_map_of_mem (sorry!)
Rename the mem_map_of_mem that you have right now to apply_coe_mem_map, and add it for submodule too. After all, the of_mem part of the name is a lie.

eric-wieser reviewed

View reviewed changes

src/group_theory/subgroup.lean Outdated Show resolved Hide resolved

riccardobrasca and others added 2 commits

May 4, 2021 11:43


          Update src/group_theory/subgroup.lean

eae903f

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>


          use apply_coe_mem_map, also for submodules

605aff6

eric-wieser reviewed

View reviewed changes

src/group_theory/subgroup.lean Outdated Show resolved Hide resolved

eric-wieser reviewed

View reviewed changes

src/group_theory/submonoid/operations.lean Outdated Show resolved Hide resolved

eric-wieser reviewed

View reviewed changes

src/linear_algebra/basic.lean Outdated Show resolved Hide resolved

riccardobrasca and others added 6 commits

May 4, 2021 12:03


          Update src/linear_algebra/basic.lean

1f502c9

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>


          Update src/group_theory/subgroup.lean

def6080

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>


          Update src/group_theory/submonoid/operations.lean

cde417a

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>


          fix build

01cee97


          fix build

d1a1f10


          fix build

299ecae

riccardobrasca mentioned this pull request

[Merged by Bors] - feat(analysis/normed_space/normed_group_hom): add lemmas #7474

Closed

1 task

riccardobrasca and others added 3 commits

May 4, 2021 13:11


          fix build

31927c4


          fix build

d2c8957


          Merge branch 'mem_map_of_mem' of github.com:leanprover-community/math…

e9a536c

…lib into mem_map_of_mem

jcommelin requested a review from eric-wieser

May 6, 2021 14:04

eric-wieser reviewed

View reviewed changes

src/group_theory/submonoid/operations.lean Outdated Show resolved Hide resolved

eric-wieser reviewed

View reviewed changes

src/ring_theory/jacobson.lean

		(ϕ.map (M.mem_map_of_mem (φ : P'.quotient →* P.quotient)) ϕ') _ _,
		(ϕ.map (submonoid.apply_coe_mem_map (φ : P'.quotient →* P.quotient)) ϕ') _ _,

Member

eric-wieser May 6, 2021

What's your preference for M being implicit vs implicit here @riccardobrasca? I'm happy either way, and only really care about consistency between the lemmas that share names. I'm fine with it as you have it now, but I'm also fine with you making s, p etc explicit in all the new lemmas.

Member Author

riccardobrasca May 6, 2021

What about leaving the variable implicit in mem_map_of_mem (that seems the standard in mathlib), but explicit in apply_coe_mem_map to allow dot notation as it is currently used?

Member Author

riccardobrasca May 6, 2021

Oh, there are a lot of mem_map_of_mem... I guess I will open another PR to add all the corresponding apply_coe_mem_map when we have decided which form is better.

Member

jcommelin May 10, 2021

I agree that this can be postponed to a later PR.

riccardobrasca and others added 2 commits

May 6, 2021 16:32


          Update src/group_theory/submonoid/operations.lean

e8cce86

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>


          Merge branch 'master' into mem_map_of_mem

8177da2

jcommelin approved these changes

View reviewed changes

Member

jcommelin left a comment

Thanks 🎉

bors merge

github-actions bot added the ready-to-merge label

github-actions bot removed the awaiting-review label

bors bot pushed a commit that referenced this pull request


          feat(group_theory/subgroup): add mem_map_of_mem (#7459)

f985e36

From LTE.

Written by @PatrickMassot 



Co-authored-by: Patrick Massot <patrickmassot@free.fr>

bors bot commented May 10, 2021

Pull request successfully merged into master.

Build succeeded:

bors bot changed the title ~~feat(group_theory/subgroup): add mem_map_of_mem~~ [Merged by Bors] - feat(group_theory/subgroup): add mem_map_of_mem

bors bot closed this

bors bot deleted the mem_map_of_mem branch

May 10, 2021 12:35

riccardobrasca mentioned this pull request

[Merged by Bors] - feat(ring_theory/ideal/operations): add apply_coe_mem_map #7566

Closed

bors bot pushed a commit that referenced this pull request


          feat(analysis/normed_space/normed_group_hom): add lemmas (#7474)

1cbb31d

From LTE.

Written by @PatrickMassot 

- [x] depends on: #7459 



Co-authored-by: Patrick Massot <patrickmassot@free.fr>

bors bot pushed a commit that referenced this pull request


          feat(ring_theory/ideal/operations): add apply_coe_mem_map (#7566)

239908e

This is a continuation of #7459. In this PR:

- We modify `ideal.mem_map_of_mem` in order to be consistent with `submonoid.mem_map_of_mem`.
- We modify `submonoid.apply_coe_mem_map` (and friends) to have the submonoid as an explicit variable. This was the case before #7459 (but with a different, and not consistent, name). It seems to me that this version makes the code more readable.
- We add `ideal.apply_coe_mem_map` (similar to `submonoid.apply_coe_mem_map`).

Note that `mem_map_of_mem` is used in other places, for example we have `multiset.mem_map_of_mem`, but since a multiset is not a type there is no `apply_coe_mem_map` to add there.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment