[Merged by Bors] - feat(Geometry/Convex): affine maps into a module form a module

[YaelDillies]

... under pointwise operations.

From the Polyhedra in Berlin workshop, where participants requested this to talk about the dual space of a convex space.

---

[github-actions]

PR summary 48d90e249b

Import changes exceeding 2%

%	File
+11.35%	Mathlib.Geometry.Convex.ConvexSpace.Module

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Geometry.Convex.ConvexSpace.Module	1040	1158	+118 (+11.35%)

Import changes for all files

Files	Import difference
Mathlib.Geometry.Convex.ConvexSpace.ModuleTopology	46
Mathlib.Geometry.Convex.ConvexSpace.Module	118
Mathlib.Geometry.Convex.AffineMap.Defs (new file)	1031
Mathlib.Geometry.Convex.AffineMap.Module (new file)	1162

---

Declarations diff (regex)

+ ConvexSpace.AffineMap.instIsModuleConvexSpace
+ IsAffineMap.const_smul
+ IsAffineMap.eval
+ IsAffineMap.finsupp
+ IsAffineMap.finsuppEval
+ IsAffineMap.fst
+ IsAffineMap.iConvexComb
+ IsAffineMap.linearMap
+ IsAffineMap.pi
+ IsAffineMap.prodMk
+ IsAffineMap.snd
+ IsConvexCombComm
+ IsConvexCombComm.instSelf
+ IsConvexCombComm.symm
+ coe_mk
+ convexCombPair_apply
+ iConvexComb_apply
+ instConvexSpace
+ instance : Add (ConvexSpace.AffineMap R X M)
+ instance : AddCommGroup (ConvexSpace.AffineMap R X M)
+ instance : AddCommMonoid (ConvexSpace.AffineMap R X M)
+ instance : FunLike (ConvexSpace.AffineMap R X Y) X Y
+ instance : IsAddApply (ConvexSpace.AffineMap R X M) X M where add_apply _ _ _ := rfl
+ instance : IsNegApply (ConvexSpace.AffineMap R X M) X M where neg_apply _ _ := rfl
+ instance : IsSMulApply S (ConvexSpace.AffineMap R X M) X M where smul_apply _ _ _ := rfl
+ instance : IsSubApply (ConvexSpace.AffineMap R X M) X M where sub_apply _ _ _ := rfl
+ instance : IsZeroApply (ConvexSpace.AffineMap R X M) X M where zero_apply _ := rfl
+ instance : Neg (ConvexSpace.AffineMap R X M)
+ instance : SMul S (ConvexSpace.AffineMap R X M) where smul s f := ⟨s • f, by fun_prop⟩
+ instance : Sub (ConvexSpace.AffineMap R X M)
+ instance : Zero (ConvexSpace.AffineMap R X M) := ⟨.const 0⟩
+ instance [ConvexSpace S X] [ConvexSpace S Y] [IsConvexCombComm R S X]
+ instance [ConvexSpace S X] [IsConvexCombComm R S X] : IsConvexCombComm R S (ι →₀ X)
+ instance [DistribMulAction Sᵐᵒᵖ M] [IsCentralScalar S M] :
+ instance [Monoid S] [DistribMulAction S M] [SMulCommClass S R M] :
+ instance [SMul S T] [IsScalarTower S T M] : IsScalarTower S T (ConvexSpace.AffineMap R X M)
+ instance [SMulCommClass S T M] : SMulCommClass S T (ConvexSpace.AffineMap R X M)
+ instance [Semiring S] [Module S M] [SMulCommClass S R M] :
+ instance [∀ i, ConvexSpace S (X i)] [∀ i, IsConvexCombComm R S (X i)] :
+ instance _root_.SMulCommClass.toIsConvexCombComm : IsConvexCombComm R S M
+ isAffineMap_add
+ isAffineMap_comp_const
+ isAffineMap_const_comp
+ isAffineMap_const_smul
+ isAffineMap_eval
+ isAffineMap_finsupp_iff
+ isAffineMap_neg
+ isAffineMap_neg_iff
+ isAffineMap_pi_iff
+ isAffineMap_prodMk_iff
+ isAffineMap_prod_iff
+ isAffineMap_sub
+ sConvexComb_apply
- instance {X Y : Type*} [ConvexSpace R X] [ConvexSpace R Y] :

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 48d90e2).

• +58 new declarations
• −0 removed declarations

+Convexity.ConvexSpace.AffineMap.coe_mk
+Convexity.ConvexSpace.AffineMap.convexCombPair_apply
+Convexity.ConvexSpace.AffineMap.iConvexComb_apply
+Convexity.ConvexSpace.AffineMap.instAdd
+Convexity.ConvexSpace.AffineMap.instAddCommGroup
+Convexity.ConvexSpace.AffineMap.instAddCommMonoid
+Convexity.ConvexSpace.AffineMap.instConvexSpace
+Convexity.ConvexSpace.AffineMap.instDistribMulActionOfSMulCommClass
+Convexity.ConvexSpace.AffineMap.instIsAddApply
+Convexity.ConvexSpace.AffineMap.instIsCentralScalar
+Convexity.ConvexSpace.AffineMap.instIsModuleConvexSpace
+Convexity.ConvexSpace.AffineMap.instIsNegApply
+Convexity.ConvexSpace.AffineMap.instIsSMulApply
+Convexity.ConvexSpace.AffineMap.instIsScalarTower
+Convexity.ConvexSpace.AffineMap.instIsSubApply
+Convexity.ConvexSpace.AffineMap.instIsZeroApply
+Convexity.ConvexSpace.AffineMap.instModuleOfSMulCommClass
+Convexity.ConvexSpace.AffineMap.instNeg
+Convexity.ConvexSpace.AffineMap.instSMul
+Convexity.ConvexSpace.AffineMap.instSMulCommClass
+Convexity.ConvexSpace.AffineMap.instSub
+Convexity.ConvexSpace.AffineMap.instZero
+Convexity.ConvexSpace.AffineMap.isAffineMap_comp_const
+Convexity.ConvexSpace.AffineMap.isAffineMap_const_comp
+Convexity.ConvexSpace.AffineMap.isAffineMap_eval
+Convexity.ConvexSpace.AffineMap.sConvexComb_apply
+Convexity.IsAffineMap.const_smul
+Convexity.IsAffineMap.eval
+Convexity.IsAffineMap.finsupp
+Convexity.IsAffineMap.finsuppEval
+Convexity.IsAffineMap.fst
+Convexity.IsAffineMap.iConvexComb
+Convexity.IsAffineMap.linearMap
+Convexity.IsAffineMap.pi
+Convexity.IsAffineMap.prodMk
+Convexity.IsAffineMap.snd
+Convexity.IsConvexCombComm
+Convexity.IsConvexCombComm.casesOn
+Convexity.IsConvexCombComm.iConvexComb_comm'
+Convexity.IsConvexCombComm.instSelf
+Convexity.IsConvexCombComm.mk
+Convexity.IsConvexCombComm.rec
+Convexity.IsConvexCombComm.recOn
+Convexity.IsConvexCombComm.symm
+Convexity.fun_isAffineMap_neg_iff
+Convexity.isAffineMap_add
+Convexity.isAffineMap_const_smul
+Convexity.isAffineMap_finsupp_iff
+Convexity.isAffineMap_neg
+Convexity.isAffineMap_neg_iff
+Convexity.isAffineMap_pi_iff
+Convexity.isAffineMap_prodMk_iff
+Convexity.isAffineMap_prod_iff
+Convexity.isAffineMap_sub
+Finsupp.instIsConvexCombComm
+Pi.instIsConvexCombCommForall
+Prod.instIsConvexCombComm
+SMulCommClass.toIsConvexCombComm

---

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
exposed public sections	5064	1

Current commit 48d90e249b
Reference commit af25e2dc5a

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[eric-wieser]

bors d+

Thanks!

[mathlib-bors]

✌️ YaelDillies can now approve this pull request until 2026-09-25 13:49 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, Wanted/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean, Wanted.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.

[eric-wieser]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Lint style
• ci (staging) / Build
• ci (staging) / Post-Build Step
• ci (staging) / Test and lint
• ci (staging) / Post-CI job