Commit 2023-05-19 05:51 20979e97

View on Github →

feat: port Analysis.NormedSpace.Extend (#4069)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/Extend.lean

added theorem ContinuousLinearMap.extendTo𝕜'_apply

added theorem ContinuousLinearMap.extendTo𝕜_apply

added theorem ContinuousLinearMap.norm_extendTo𝕜'

added theorem ContinuousLinearMap.norm_extendTo𝕜'_bound

added theorem ContinuousLinearMap.norm_extendTo𝕜

added theorem LinearMap.extendTo𝕜'_apply

added theorem LinearMap.extendTo𝕜'_apply_re

added theorem LinearMap.extendTo𝕜_apply

added theorem LinearMap.norm_extendTo𝕜'_apply_sq