Commit 2024-07-30 16:56 245de8ad

View on Github →

chore(NormedSpace/Multilinear): drop DecidableEq assumptions (#15268)

Estimated changes

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

modified theorem ContinuousMultilinearMap.iteratedFDerivComponent_apply

modified theorem ContinuousMultilinearMap.norm_iteratedFDerivComponent_le