# 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.