Theorem isBoundedBilinearMapApply

Modification history

2023-09-05 12:17

Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean

chore: rename isBoundedBilinearMapApply to isBoundedBilinearMap_apply (#6963)

Deleted isBoundedBilinearMapApply View on Github →

2023-05-20 10:55

Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean

feat: port Analysis.NormedSpace.BoundedLinearMaps (#4091) …

Added isBoundedBilinearMapApply View on Github →