is_derive_mulmx

[yosakaon]

Motivation for this change

This PR completes #1891 (comment) with is_derive for matrix multiplication.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[yosakaon]

it is worth noting that Hint Extern 0 (is_derive _ _ (fun x => _ *m _) _) => apply: is_derive_mulmx : typeclass_instances. will help solve harder goals while leaving simple apply fails!

[affeldt-aist]

it is worth noting that Hint Extern 0 (is_derive _ _ (fun x => _ *m _) _) => apply: is_derive_mulmx : typeclass_instances. will help solve harder goals while leaving simple apply fails!

Do you want to do something about this in this PR or produce an issue to deal with it later?
(I am asking for the release of MathComp-Analysis 1.17.0.)

[affeldt-aist]

I created an issue (#2069) so that we can merge without forgetting about your observation.