Commit 2025-10-29 10:55 188562f5
View on Github →chore: make MDifferentiableAt.mfderiv_prod an alias. (#31048) It duplicates a lemma above, but having this name is nice for discoverability.
chore: make MDifferentiableAt.mfderiv_prod an alias. (#31048) It duplicates a lemma above, but having this name is nice for discoverability.