mathlib3

2b7b1e72 - refactor(algebra/group/inj_surj): eliminate the versions of the definitions without `has_div` / `has_sub`. (#7035)

refactor(algebra/group/inj_surj): eliminate the versions of the definitions without `has_div` / `has_sub`. (#7035) The variables without the `_sub` / `_div` suffix were vestigial definitions that existed in order to prevent the already-large `div_inv_monoid` refactor becoming larger. This change removes all their remaining usages, allowing the `_sub` / `_div` versions to lose their suffix. This changes the division operation on `α →ₘ[μ] γ` and the subtraction operator on `truncated_witt_vector p n R` to definitionally match the division operation on their components. In practice, this just shuffles some uses of `sub_eq_add_neg` around.