mathlib3

8e46fa5a - chore(algebra/group/to_additive): map_namespace should make a meta constant (#1409)

chore(algebra/group/to_additive): map_namespace should make a meta constant (#1409) * chore(algebra/group/to_additive): map_namespace should make a meta constance `map_namespace` now produces a `meta constant` instead of a constant. This means that after importing `group_theory/coset` and typing `#print axioms`, `quotient_group._to_additive` is not in the list, since it is now a `meta constant`. This is a little bit neater, and it doesn't look like we're adding any axioms. * Update to_additive.lean * Update to_additive.lean