Def IsBoundedBilinearMap.linearDeriv

Modification history

2023-05-25 03:53

Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean

chore: golf proofs about `IsBoundedBilinearMap` (#4239) …

Modified IsBoundedBilinearMap.linearDeriv View on Github →

2023-05-20 10:55

Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean

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

Added IsBoundedBilinearMap.linearDeriv View on Github →