Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-05-17 22:42
8bf78812
View on Github →
feat: port Analysis.NormedSpace.IsROrC (
#4055
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Analysis/NormedSpace/IsROrC.lean
added
theorem
ContinuousLinearMap.op_norm_bound_of_ball_bound
added
theorem
IsROrC.norm_coe_norm
added
theorem
LinearMap.bound_of_ball_bound'
added
theorem
LinearMap.bound_of_sphere_bound
added
theorem
NormedSpace.sphere_nonempty_isROrC
added
theorem
norm_smul_inv_norm'
added
theorem
norm_smul_inv_norm