Theorem isBoundedBilinearMapSmulRight

Modification history

2023-06-02 11:44

Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean

chore: fix some names (#4564) …

Deleted isBoundedBilinearMapSmulRight View on Github →

2023-05-20 10:55

Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean

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

Added isBoundedBilinearMapSmulRight View on Github →