smul_mem_center — Mathlib

English

If an element a lies in the center of A, then any scalar multiple r·a also lies in the center.

Русский

Если a лежит в центре алгебры, то любая скалярная кратность r·a также лежит в центре.

LaTeX

$$$a \in \mathrm{center}(A) \Rightarrow (r a) \in \mathrm{center}(A)$$$

Lean4

theorem _root_.Set.smul_mem_center (r : R) {a : A} (ha : a ∈ Set.center A) : r • a ∈ Set.center A
    where
  comm b := by rw [commute_iff_eq, mul_smul_comm, smul_mul_assoc, ha.comm]
  left_assoc b c := by rw [smul_mul_assoc, smul_mul_assoc, smul_mul_assoc, ha.left_assoc]
  right_assoc b c := by rw [mul_smul_comm, mul_smul_comm, mul_smul_comm, ha.right_assoc]

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