mathlib3

07b5618a - chore(linear_algebra/{multilinear,alternating}): Generalize smul and neg instance (#5364)

chore(linear_algebra/{multilinear,alternating}): Generalize smul and neg instance (#5364) This brings the generality in line with that of `linear_map`. Notably: * `has_neg` now exists when only the codomain has negation * `has_scalar` now exists for the weaker condition of `smul_comm_class` rather than `has_scalar_tower`