right_comm — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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