mathlib

7f103fd3 - fix(tactic/transport): make `to_additive` copy `protected`status (#2212)

fix(tactic/transport): make `to_additive` copy `protected`status (#2212) * fix(tactic/transport): make `to_additive` copy `protected`status Fixes #2210, also slightly cleanup `algebra/group/units` * Fix compile (protected `finset.sum`) * Fix usage of `finset.sum` * Update src/tactic/transport.lean Co-Authored-By: Gabriel Ebner <gebner@gebner.org> * fix build Co-authored-by: Gabriel Ebner <gebner@gebner.org> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>