Commit 2024-07-12 20:12 e539139d

View on Github →

feat: Translation of affine bases (#14682) Provide the additive action of a module V over the k-affine bases of a V-torsor P.

Estimated changes

Modified Mathlib/Data/Set/Pointwise/SMul.lean

added theorem Set.range_mul

added theorem Set.range_smul

modified theorem Set.smul_set_range

Modified Mathlib/LinearAlgebra/AffineSpace/Basis.lean

added theorem AffineBasis.basisOf_vadd

added theorem AffineBasis.coe_vadd

added theorem AffineBasis.coord_vadd

Modified Mathlib/LinearAlgebra/AffineSpace/Combination.lean

added theorem Finset.weightedVSubOfPoint_vadd

added theorem Finset.weightedVSub_vadd

Modified Mathlib/LinearAlgebra/AffineSpace/Independent.lean

added theorem affineIndependent_vadd

Modified Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean

modified theorem AffineSubspace.pointwise_vadd_bot

added theorem AffineSubspace.pointwise_vadd_top