coe_pointwise_smul — Mathlib

English

The underlying set of the submodule a · S equals the pointwise action of a on the underlying set of S; i.e., the elements of a · S are exactly {a · x : x ∈ S}.

Русский

Лежащая в основе множество подмодуля a · S равно множеству {a · x : x ∈ S}.

LaTeX

$$$\\uparrow(a \\cdot S) = a \\cdot (S : Set M)$$$

Lean4

@[simp, norm_cast]
theorem coe_pointwise_smul (a : α) (S : Submodule R M) : ↑(a • S) = a • (S : Set M) :=
  rfl

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