English
For any t ⊆ P with a certain affine span property, there exists a subset s ⊆ t and an AffineBasis s such that the basis map equals the inclusion on s.
Русский
Для любого t ⊆ P с заданным свойством аффинного охвата существует подмножество s ⊆ t и аффинная база b над s такая, что b = включение на s.
LaTeX
$$$\\exists s \\subseteq t,\\; \\exists b : AffineBasis\\, s\\ k P,\\; \\forall x \\in s:\\; b(x) = x$$$
Lean4
/-- In an affine space that is also a vector space, an `AffineBasis` can be scaled.
TODO: generalize to include `SMul (P ≃ᵃ[k] P) (AffineBasis ι k P)`, which acts on `P` with a `VAdd`
version of a `DistribMulAction`. -/
instance instSMul : SMul G (AffineBasis ι k V) where
smul a
b :=
{ toFun := a • ⇑b, ind' := b.ind'.smul,
tot' := by
rw [Pi.smul_def, ← smul_set_range, ← AffineSubspace.smul_span, b.tot,
AffineSubspace.smul_top (Group.isUnit a)] }
