smul_of

Mathlib.Algebra.SkewMonoidAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#SkewMonoidAlgebra.smul_of

English

For g ∈ G and r ∈ k, the scalar action satisfies r • of(k,G,g) = single g r.

Русский

Для элемента g ∈ G и скаляра r ∈ k выполнено r • t = single g r, где t = of k G g.

LaTeX

$$$ r \cdot \mathrm{of}\; k\; G\; g = \mathrm{single}\; g\; r $$$

Lean4

theorem smul_of (g : G) (r : k) : r • of k G g = single g r := by rw [of_apply, smul_single, smul_eq_mul, mul_one]

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

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

Разделы

Аффилиация

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