Commit 2025-09-23 19:02 05514c8f

View on Github →

chore: generalize ContinuousAffineMap.contLinear to IsTopologicalAddTorsor (#29617)

Estimated changes

Modified Mathlib/Analysis/Calculus/AddTorsor/AffineMap.lean

Modified Mathlib/Analysis/Normed/Affine/ContinuousAffineMap.lean

deleted theorem ContinuousAffineMap.add_contLinear

deleted theorem ContinuousAffineMap.coe_contLinear

deleted theorem ContinuousAffineMap.coe_contLinear_eq_linear

deleted theorem ContinuousAffineMap.coe_linear_eq_coe_contLinear

deleted theorem ContinuousAffineMap.coe_mk_const_linear_eq_linear

deleted theorem ContinuousAffineMap.comp_contLinear

deleted theorem ContinuousAffineMap.const_contLinear

deleted def ContinuousAffineMap.contLinear

deleted theorem ContinuousAffineMap.contLinear_eq_zero_iff_exists_const

deleted theorem ContinuousAffineMap.contLinear_map_vsub

deleted theorem ContinuousAffineMap.decomp

deleted theorem ContinuousAffineMap.map_vadd

deleted theorem ContinuousAffineMap.neg_contLinear

deleted theorem ContinuousAffineMap.prodMap_contLinear

deleted theorem ContinuousAffineMap.prod_contLinear

deleted theorem ContinuousAffineMap.smul_contLinear

deleted theorem ContinuousAffineMap.sub_contLinear

deleted theorem ContinuousAffineMap.to_affine_map_contLinear

deleted theorem ContinuousAffineMap.vadd_apply

deleted theorem ContinuousAffineMap.vadd_toAffineMap

deleted theorem ContinuousAffineMap.vsub_apply

deleted theorem ContinuousAffineMap.vsub_toAffineMap

deleted theorem ContinuousAffineMap.zero_contLinear

Modified Mathlib/Geometry/Euclidean/Projection.lean

Modified Mathlib/Topology/Algebra/ContinuousAffineMap.lean

added theorem ContinuousAffineMap.add_contLinear

added theorem ContinuousAffineMap.coe_contLinear

added theorem ContinuousAffineMap.coe_contLinear_eq_linear

added theorem ContinuousAffineMap.coe_linear_eq_coe_contLinear

added theorem ContinuousAffineMap.coe_mk_contLinear_eq_linear

added theorem ContinuousAffineMap.comp_contLinear

added theorem ContinuousAffineMap.const_contLinear

added def ContinuousAffineMap.contLinear

added theorem ContinuousAffineMap.contLinear_eq_zero_iff_exists_const

added theorem ContinuousAffineMap.contLinear_map_vsub

added theorem ContinuousAffineMap.decomp

added theorem ContinuousAffineMap.map_vadd

added theorem ContinuousAffineMap.neg_contLinear

added theorem ContinuousAffineMap.prodMap_contLinear

added theorem ContinuousAffineMap.prod_contLinear

added theorem ContinuousAffineMap.smul_contLinear

added theorem ContinuousAffineMap.sub_contLinear

added theorem ContinuousAffineMap.vadd_apply

added theorem ContinuousAffineMap.vadd_contLinear

added theorem ContinuousAffineMap.vadd_toAffineMap

added theorem ContinuousAffineMap.vsub_apply

added theorem ContinuousAffineMap.vsub_contLinear

added theorem ContinuousAffineMap.vsub_toAffineMap

added theorem ContinuousAffineMap.zero_contLinear

added theorem ContinuousLinearMap.toContinuousAffineMap_contLinear