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.

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(*): define equiv.reflection and isometry.reflection #2609

Closed
wants to merge 7 commits into from
Closed

[Merged by Bors] - feat(*): define equiv.reflection and isometry.reflection #2609

wants to merge 7 commits into from

Conversation

urkud
Copy link
Member

@urkud urkud commented May 5, 2020

Define reflection in a point and prove basic properties.
It is defined both as an equiv.perm of an add_comm_group and
as an isometric of a normed_group.

Other changes:

  • rename two_smul to two_smul', add two_smul using semimodule
    instead of add_monoid.smul;
  • minor review of algebra.midpoint;
  • arguments of isometry.dist_eq and isometry.edist_eq are now explicit;
  • rename isometry.inv to isometry.right_inv; now it takes right_inverse
    instead of equiv;
  • drop isometry_inv_fun: use h.symm.isometry instead;
  • pull a few more lemmas about equiv and isometry to the isometric namespace.

@urkud urkud added the awaiting-review The author would like community review of the PR label May 6, 2020
@urkud urkud mentioned this pull request May 6, 2020
Closed
sgouezel
sgouezel reviewed May 6, 2020
View reviewed changes
src/analysis/normed_space/reflection.lean Show resolved Hide resolved
src/analysis/normed_space/reflection.lean Outdated Show resolved Hide resolved
src/analysis/normed_space/reflection.lean Show resolved Hide resolved
src/data/equiv/mul_add.lean Outdated Show resolved Hide resolved
@sgouezel sgouezel 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 May 6, 2020
@urkud urkud added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels May 6, 2020
@sgouezel sgouezel 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 May 6, 2020
@urkud urkud added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels May 7, 2020
@sgouezel
Copy link
Collaborator

sgouezel commented May 7, 2020

bors r+

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels May 7, 2020
bors bot pushed a commit that referenced this pull request May 7, 2020
@urkud
feat(*): define equiv.reflection and isometry.reflection (#2609)
da10afc 
Define reflection in a point and prove basic properties.
It is defined both as an `equiv.perm` of an `add_comm_group` and
as an `isometric` of a `normed_group`.

Other changes:

* rename `two_smul` to `two_smul'`, add `two_smul` using `semimodule`
  instead of `add_monoid.smul`;
* minor review of `algebra.midpoint`;
* arguments of `isometry.dist_eq` and `isometry.edist_eq` are now explicit;
* rename `isometry.inv` to `isometry.right_inv`; now it takes `right_inverse`
  instead of `equiv`;
* drop `isometry_inv_fun`: use `h.symm.isometry` instead;
* pull a few more lemmas about `equiv` and `isometry` to the `isometric` namespace.
@bors
Copy link

bors bot commented May 7, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(*): define equiv.reflection and isometry.reflection [Merged by Bors] - feat(*): define equiv.reflection and isometry.reflection May 7, 2020
@bors bors bot closed this May 7, 2020
@bors bors bot deleted the reflection branch May 7, 2020 13:09
anrddh pushed a commit to anrddh/mathlib that referenced this pull request May 15, 2020
@urkud @anrddh
feat(*): define equiv.reflection and isometry.reflection (leanpro…
4c45924 
…ver-community#2609)

Define reflection in a point and prove basic properties.
It is defined both as an `equiv.perm` of an `add_comm_group` and
as an `isometric` of a `normed_group`.

Other changes:

* rename `two_smul` to `two_smul'`, add `two_smul` using `semimodule`
  instead of `add_monoid.smul`;
* minor review of `algebra.midpoint`;
* arguments of `isometry.dist_eq` and `isometry.edist_eq` are now explicit;
* rename `isometry.inv` to `isometry.right_inv`; now it takes `right_inverse`
  instead of `equiv`;
* drop `isometry_inv_fun`: use `h.symm.isometry` instead;
* pull a few more lemmas about `equiv` and `isometry` to the `isometric` namespace.
anrddh pushed a commit to anrddh/mathlib that referenced this pull request May 16, 2020
@urkud @anrddh
feat(*): define equiv.reflection and isometry.reflection (leanpro…
413daf3 
…ver-community#2609)

Define reflection in a point and prove basic properties.
It is defined both as an `equiv.perm` of an `add_comm_group` and
as an `isometric` of a `normed_group`.

Other changes:

* rename `two_smul` to `two_smul'`, add `two_smul` using `semimodule`
  instead of `add_monoid.smul`;
* minor review of `algebra.midpoint`;
* arguments of `isometry.dist_eq` and `isometry.edist_eq` are now explicit;
* rename `isometry.inv` to `isometry.right_inv`; now it takes `right_inverse`
  instead of `equiv`;
* drop `isometry_inv_fun`: use `h.symm.isometry` instead;
* pull a few more lemmas about `equiv` and `isometry` to the `isometric` namespace.
cipher1024 pushed a commit to cipher1024/mathlib that referenced this pull request Mar 15, 2022
@urkud @cipher1024
feat(*): define equiv.reflection and isometry.reflection (leanpro…
9d0edf5 
…ver-community#2609)

Define reflection in a point and prove basic properties.
It is defined both as an `equiv.perm` of an `add_comm_group` and
as an `isometric` of a `normed_group`.

Other changes:

* rename `two_smul` to `two_smul'`, add `two_smul` using `semimodule`
  instead of `add_monoid.smul`;
* minor review of `algebra.midpoint`;
* arguments of `isometry.dist_eq` and `isometry.edist_eq` are now explicit;
* rename `isometry.inv` to `isometry.right_inv`; now it takes `right_inverse`
  instead of `equiv`;
* drop `isometry_inv_fun`: use `h.symm.isometry` instead;
* pull a few more lemmas about `equiv` and `isometry` to the `isometric` namespace.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@sgouezel sgouezel sgouezel left review comments

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@urkud @sgouezel