Commit 2020-05-07 10:25 da10afcf

View on Github →

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

Estimated changes