Commit 2020-12-14 16:39 07b5618a

View on Github →

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

Estimated changes

Modified src/linear_algebra/alternating.lean

added theorem alternating_map.map_neg

modified theorem alternating_map.neg_apply

modified theorem alternating_map.to_multilinear_map_alternization

modified def multilinear_map.alternatization

modified theorem multilinear_map.alternatization_apply

Modified src/linear_algebra/multilinear.lean

added theorem multilinear_map.map_neg