Commit 2025-11-21 04:24 7df67282

View on Github →

chore: make CLM.extend total and define LM.leftInverse (#31799)

Make ContinuousLinearMap.extend a total function
Define LinearMap.leftInverse as a total function with junk value if the input is not invertible. Required for #31074

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/LinearPMap.lean

modified theorem LinearPMap.adjointDomainMkCLMExtend_apply

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

modified theorem ContinuousLinearMap.extend_eq

modified theorem ContinuousLinearMap.extend_unique

modified theorem ContinuousLinearMap.extend_zero

modified theorem ContinuousLinearMap.opNorm_extend_le

Modified Mathlib/LinearAlgebra/Basis/VectorSpace.lean

added def LinearMap.leftInverse

added theorem LinearMap.leftInverse_apply_of_inj

added theorem LinearMap.leftInverse_comp_of_inj

Modified Mathlib/LinearAlgebra/Dual/Lemmas.lean

Modified Mathlib/MeasureTheory/Function/Holder.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/L1.lean

added theorem MeasureTheory.L1.SimpleFunc.integralCLM'_L1_eq_integral

added theorem MeasureTheory.L1.integral_eq'

Modified Mathlib/MeasureTheory/Integral/SetToL1.lean

added theorem MeasureTheory.L1.setToL1'_apply_coeToLp

added theorem MeasureTheory.L1.setToL1'_eq_setToL1SCLM

added theorem MeasureTheory.L1.setToL1_apply_coeToLp

added theorem MeasureTheory.L1.setToL1_unique

Modified Mathlib/RepresentationTheory/Maschke.lean