Theorem is_unit_iff_exists_inv'

feat(algebra/group/to_additive + a few more files): make `to_additive` convert `unit` to `add_unit` (#12564) …

refactor(algebra): merge init_.algebra into algebra (#2707) …

feat(group_theory/monoid_localization): some homs induced on localizations: lift, map (#2118) …

refactor(group_theory/monoid_localization): use characteristic predicate (#2004) …

refactor(algebra/associated): move `is_unit` def to `algebra/group` (#2015) …

feat(linear_algebra,ring_theory): refactoring modules (#456) …