zsmul_eq_mul' — Mathlib

English

For any α in a nonassociative ring, and any integer n, zsmul by n equals a times n on the right: n • a = a * n.

Русский

Для любого кольца без ассоциативности и любого целого n, n • a = a * n.

LaTeX

$$$ \forall {\alpha} [NonAssocRing \alpha], \forall a \in \alpha, \forall n \in \mathbb{Z}, n \cdot a = a \cdot n$$$

Lean4

theorem _root_.zsmul_eq_mul' (a : α) (n : ℤ) : n • a = a * n := by rw [zsmul_eq_mul, (n.cast_commute a).eq]

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