Commit 2026-09-16 15:44 5d90fca6

View on Github →

chore: make m(v)fderiv(Within)_eq_fderiv(Within) more type-correct (#43521)

Estimated changes

modified theorem mfderiv_eq_fderiv
modified theorem mvfderiv_eq_fderiv