coe_pointwise_smul — Mathlib

English

The coercion map commutes with pointwise smul: the underlying set of m • S equals m • (S as a set).

Русский

Коэрцируемое отображение сохраняет точечное умножение: множество подмножества размером m • S совпадает с m • (множество S).

LaTeX

$$$ \uparrow( m \cdot S) = m \cdot (S) $$$

Lean4

@[simp, norm_cast]
theorem coe_pointwise_smul (m : M) (S : AddSubmonoid A) : ↑(m • S) = m • (S : Set A) :=
  rfl

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