Theorem ContinuousAffineMap.norm_def

Modification history

2023-06-09 09:11

Mathlib/Analysis/NormedSpace/ContinuousAffineMap.lean

feat: port Analysis.NormedSpace.ContinuousAffineMap (#4867)

Added ContinuousAffineMap.norm_def View on Github →