Commit 2024-08-13 09:00 b1130920

View on Github →

feat: Scaling of affine bases (#14863) Given a group G acting on the ring k, provide the G-action over the k-affine bases of a k-module V.

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/Basis.lean

added theorem AffineBasis.basisOf_smul

added theorem AffineBasis.coe_smul

added theorem AffineBasis.coord_smul

added theorem AffineBasis.reindex_smul

Modified Mathlib/LinearAlgebra/AffineSpace/Combination.lean

added theorem Finset.weightedVSubOfPoint_smul

added theorem Finset.weightedVSub_smul

Modified Mathlib/LinearAlgebra/AffineSpace/Independent.lean

added theorem affineIndependent_smul

Modified Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean

modified theorem AffineSubspace.coe_pointwise_vadd

added theorem AffineSubspace.coe_smul

added theorem AffineSubspace.direction_smul

added theorem AffineSubspace.smul_bot

added theorem AffineSubspace.smul_eq_map

added theorem AffineSubspace.smul_mem_smul_iff

added theorem AffineSubspace.smul_mem_smul_iff_of_isUnit

added theorem AffineSubspace.smul_mem_smul_iff₀

added theorem AffineSubspace.smul_span

added theorem AffineSubspace.smul_top