intIsScalarTower — Mathlib

English

There is an IsScalarTower Int R M, i.e. the integers act compatibly with the R-action on M: (n • r) • m = n • (r • m) for all n ∈ ℤ, r ∈ R, m ∈ M.

Русский

Существует IsScalarTower Int R M: целые числа действуют согласованно с действием R на M: (n • r) • m = n • (r • m).

LaTeX

$$$\\mathrm{IsScalarTower}\\ \\mathbb{Z}\\ R\\ M$$$

Lean4

instance intIsScalarTower {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] : IsScalarTower ℤ R M where
  smul_assoc n x
    y := by
    cases n with
    | ofNat => simp [mul_smul, Nat.cast_smul_eq_nsmul]
    | negSucc => simp [mul_smul, add_smul, Nat.cast_smul_eq_nsmul]

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