Commit 2025-08-30 09:10 f0f1d7c4

View on Github →

feat: products of affine maps (#28662) This PR defines some maps and isomorphisms between products of affine spaces.

Estimated changes

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

added theorem ContinuousAffineMap.prodMap_contLinear

added theorem ContinuousAffineMap.prod_contLinear

Modified Mathlib/Analysis/Normed/Group/AddTorsor.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean

added theorem AffineEquiv.coe_prodCongr

added def AffineEquiv.prodAssoc

added def AffineEquiv.prodComm

added theorem AffineEquiv.prodComm_symm

added def AffineEquiv.prodCongr

added theorem AffineEquiv.prodCongr_apply

added theorem AffineEquiv.prodCongr_symm

Modified Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

added theorem AffineMap.coe_prod

added theorem AffineMap.coe_prodMap

added def AffineMap.prod

added def AffineMap.prodMap

added theorem AffineMap.prodMap_apply

added theorem AffineMap.prod_apply

Modified Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean

added def ContinuousAffineEquiv.prodAssoc

added def ContinuousAffineEquiv.prodComm

added theorem ContinuousAffineEquiv.prodComm_symm

added def ContinuousAffineEquiv.prodCongr

added theorem ContinuousAffineEquiv.prodCongr_apply

added theorem ContinuousAffineEquiv.prodCongr_symm

added theorem ContinuousAffineEquiv.prodCongr_toContinuousAffineMap

Modified Mathlib/Topology/Algebra/ContinuousAffineMap.lean

added theorem ContinuousAffineMap.coe_prod

added theorem ContinuousAffineMap.coe_prodMap

added def ContinuousAffineMap.prod

added def ContinuousAffineMap.prodMap

added theorem ContinuousAffineMap.prodMap_apply

added theorem ContinuousAffineMap.prod_apply