Commit 2021-04-06 13:27 2b7b1e72

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.