Commit 2025-11-30 17:00 f8aeccd2

View on Github →

feat: inl and inr as linear isometries (#32249)

Estimated changes

Modified Mathlib/Analysis/Normed/Operator/NormedSpace.lean

added theorem ContinuousLinearMap.norm_inl

added theorem ContinuousLinearMap.norm_inl_le_one

added theorem ContinuousLinearMap.norm_inr

added theorem ContinuousLinearMap.norm_inr_le_one

added theorem LinearIsometry.inl_apply

added theorem LinearIsometry.inr_apply