cast_smul_eq_zsmul — Mathlib

English

For any M with an R-module structure and any n ∈ ℤ, casting n into R and acting on M equals the zsmul by n: (n : R) • b = n • b.

Русский

Для любого M с модулем над R и любой n ∈ ℤ приводимое к R действие на b равно zsmul на n: (n : R) • b = n • b.

LaTeX

$$$\\forall (R) {M} [\\text{Ring } R] [\\text{AddCommGroup } M] [\\text{Module } R M] (n : \\mathbb{Z}) (b : M), (n : R) \\cdot b = n \\cdot b$$$

Lean4

/-- `zsmul` is equal to any other module structure via a cast. -/
@[norm_cast]
theorem cast_smul_eq_zsmul (n : ℤ) (b : M) : (n : R) • b = n • b := by
  cases n with
  | ofNat => simp [Nat.cast_smul_eq_nsmul]
  | negSucc => simp [add_smul, Nat.cast_smul_eq_nsmul]

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