Commit 2025-10-30 10:55 dbf90e0d

View on Github →

chore(Analysis/Normed/Operator): move extension to a new file (#29888) The moved parts are not modified except for adapting the sections and imports. Original definition of ContinuousLinearMap.extend was by Zhouhang Zhou in 2019 (mathlib3 PR #1649)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/InnerProductSpace/LinearPMap.lean

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

deleted def ContinuousLinearMap.extend

deleted theorem ContinuousLinearMap.extend_eq

deleted theorem ContinuousLinearMap.extend_unique

deleted theorem ContinuousLinearMap.extend_zero

deleted theorem ContinuousLinearMap.opNorm_extend_le

Created Mathlib/Analysis/Normed/Operator/Extend.lean

added def ContinuousLinearMap.extend

added theorem ContinuousLinearMap.extend_eq

added theorem ContinuousLinearMap.extend_unique

added theorem ContinuousLinearMap.extend_zero

added theorem ContinuousLinearMap.opNorm_extend_le

Modified Mathlib/MeasureTheory/Integral/SetToL1.lean