Commit 2025-11-04 14:52 242077a4

feat(LinearAlgebra/AffineSpace): affine maps/equivs determined by values on spanning sets (#30949) This PR adds extensionality lemmas showing that affine maps and equivalences are uniquely determined by their values on any set that affinely spans the entire space. All theorems are in Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic:

• AffineMap.linear_eqOn_vectorSpan: If two affine maps agree on a set, their linear parts agree on the vector span
• AffineMap.eqOn_affineSpan: Two affine maps which agree on a set, agree on its affine span
• AffineMap.ext_on: If two affine maps agree on a set that spans the entire space, they are equal
• AffineEquiv.ext_on: If two affine equivalences agree on a set that spans the entire space, they are equal (generalized to work between different spaces) Extracted from #30854.