zsmul_eq_mul — Mathlib

English

For any α in a nonassociative ring and any integer n, the zsmul of a by n equals n times a in the ring, i.e., n • a = n * a.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem _root_.zsmul_eq_mul (a : α) : ∀ n : ℤ, n • a = n * a
  | (n : ℕ) => by rw [natCast_zsmul, nsmul_eq_mul, Int.cast_natCast]
  | -[n+1] => by simp [Nat.cast_succ, neg_add_rev, Int.cast_negSucc, add_mul]

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