mathlib

e0ca8534 - feat(algebra/group/units): teach `simps` about `units` (#8204)

feat(algebra/group/units): teach `simps` about `units` (#8204) This also introduces `units.copy` to match `invertible.copy`, and uses it to make some lemmas in normed_space/units true by `rfl` (and generated by `simps`).