mul_smul_comm — Mathlib

English

For s ∈ R and x,y ∈ A, x · s • y = s • (x · y).

Русский

Для s ∈ R и x,y ∈ A выполняется x · s • y = s • (x · y).

LaTeX

$$$x \cdot (s \cdot y) = s \cdot (x \cdot y)$$$

Lean4

/-- This is just a special case of the global `mul_smul_comm` lemma that requires less typeclass
search (and was here first). -/
@[simp]
protected theorem mul_smul_comm (s : R) (x y : A) : x * s • y = s • (x * y) := by rw [smul_def, smul_def, left_comm]

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