left_comm — Mathlib

English

For x, y ∈ A and r ∈ R, x · (algebraMap R A r · y) = algebraMap R A r · (x · y).

Русский

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

LaTeX

$$$x \cdot (\operatorname{algebraMap}(R,A)(r) \cdot y) = \operatorname{algebraMap}(R,A)(r) \cdot (x \cdot y)$$$

Lean4

/-- `mul_left_comm` for `Algebra`s when one element is from the base ring. -/
theorem left_comm (x : A) (r : R) (y : A) : x * (algebraMap R A r * y) = algebraMap R A r * (x * y) := by
  rw [← mul_assoc, ← commutes, mul_assoc]

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