English
For a Ring R and AddCommGroup M with an R-action, the integers form a scalar tower: IsScalarTower Int R M, i.e. (n • r) • m = n • (r • m) for all n ∈ ℤ, r ∈ R, m ∈ M.
Русский
Для кольца R и AddCommGroup M с действием по R числа образуют скаляровую башню: IsScalarTower Int R M, то есть (n • r) • m = n • (r • m) для всех n ∈ ℤ, r ∈ R, m ∈ M.
LaTeX
$$$\\forall n \\in \\mathbb{Z},\\ r \\in R,\\ m \\in M,\\ (n \\cdot r) \\cdot m = n \\cdot (r \\cdot m)$$$
Lean4
/-- All `ℤ`-module structures are equal. Not an instance since in mathlib all `AddCommGroup`
should normally have exactly one `ℤ`-module structure by design. -/
def uniqueIntModule : Unique (Module ℤ M) where
default := inferInstance
uniq P := (Module.ext' P _) fun n => by convert int_smul_eq_zsmul P n
