smul_eq_map — Mathlib

English

The action on an affine subspace is equal to mapping by the corresponding linear map; i.e., a • s = s.map (DistribMulAction.toLinearMap k _ a).toAffineMap.

Русский

Действие на афинном подпрощранстве равно отображению через соответствующую линейную карту.

LaTeX

$$$ a \\cdot s = s.map\\bigl( (\\mathrm{DistribMulAction.toLinearMap}\\ k\\ V\\ a).toAffineMap \\bigr) $$$

Lean4

theorem smul_eq_map (a : M) (s : AffineSubspace k V) : a • s = s.map (DistribMulAction.toLinearMap k _ a).toAffineMap :=
  rfl

Похожие утверждения