Commit 2023-09-05 12:17 5498737f

View on Github →

chore: rename isBoundedBilinearMapApply to isBoundedBilinearMap_apply (#6963)

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff.lean

Modified Mathlib/Analysis/Calculus/ContDiffDef.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Measurable.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Mul.lean

Modified Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean

deleted theorem isBoundedBilinearMapApply

added theorem isBoundedBilinearMap_apply

Modified Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

Modified Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean

Modified Mathlib/Topology/VectorBundle/Basic.lean