mul_smul_one — Mathlib

English

Let y ∈ N, x ∈ M, under SMulCommClass M N N we have y * x • 1 = x • y, i.e., the order of applying smul and multiplication can be swapped under the commutation assumptions.

Русский

Пусть y ∈ N, x ∈ M; при условиях SMulCommClass выполнено y * (x • 1) = x • y, то есть можно поменять местами умножение и действие под условием коммутативности.

LaTeX

$$$ y \cdot (x \cdot 1_N) = x \cdot y $$$

Lean4

@[to_additive (attr := simp)]
theorem mul_smul_one {M N} [MulOneClass N] [SMul M N] [SMulCommClass M N N] (x : M) (y : N) : y * x • (1 : N) = x • y :=
  by rw [← smul_eq_mul, ← smul_comm, smul_eq_mul, mul_one]

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