coe_smul — Mathlib

English

The scalar action on an affine subspace commutes with the coercion to sets: the underlying set of a · s is a · (s as a set).

Русский

Действие скаляра на афинное подпространство совместимо с проецированием в множества: множество a·s равно a · (s как множество).

LaTeX

$$$ \\uparrow( a \\cdot s) = a \\cdot (s : \\mathrm{Set} \\, V) $$$

Lean4

@[simp, norm_cast]
theorem coe_smul (a : M) (s : AffineSubspace k V) : ↑(a • s) = a • (s : Set V) :=
  rfl

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