Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-02-15 16:42
0a7e5914
View on Github →
chore(FDeriv/Mul): drop unneeded DecidableEq assumptions (
#21897
) Found by the linters in
#10235
Estimated changes
Modified
Mathlib/Analysis/Calculus/FDeriv/Mul.lean
modified
theorem
hasFDerivAt_list_prod_attach'
modified
theorem
hasStrictFDerivAt_list_prod_attach'