Commit 2020-05-07 10:25 da10afcf

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.