smul_mem

Mathlib.Algebra.Star.Subalgebra

URI: https://scilib.ai/kg/mathlib#StarSubalgebra.smul_mem

English

If x ∈ S and r ∈ R, then r • x ∈ S.

Русский

Если x ∈ S и r ∈ R, то r·x ∈ S.

LaTeX

$$$\forall x \in S, \; \forall r \in R:\; r \cdot x \in S$$$

Lean4

protected theorem smul_mem {x : A} (hx : x ∈ S) (r : R) : r • x ∈ S :=
  (Algebra.smul_def r x).symm ▸ mul_mem (S.algebraMap_mem r) hx

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru