smul_mem

Mathlib.Algebra.Lie.Subalgebra

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

English

If x ∈ L' and t ∈ R, then t•x ∈ L'.

Русский

Если x ∈ L' и t ∈ R, то t•x ∈ L'.

LaTeX

$$$x \in L' \Rightarrow t \cdot x \in L'$ for all t ∈ R$$

Lean4

protected theorem smul_mem (t : R) {x : L} (h : x ∈ L') : t • x ∈ L' :=
  SMulMemClass.smul_mem _ h

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

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

Разделы

Аффилиация

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