int_isScalarTower — Mathlib

English

If R is a nonunital nonassociative ring, the integer action forms a scalar tower with R on itself.

Русский

Если R — некольцевое кольцо без единицы, целые образуют скалярную башню с R на себе.

LaTeX

$$IsScalarTower Int R R$$

Lean4

/-- Note that `AddCommGroup.int_isScalarTower` requires stronger assumptions on `R`. -/
instance int_isScalarTower [NonUnitalNonAssocRing R] : IsScalarTower ℤ R R where
  smul_assoc n x
    y :=
    match n with
    | (n : ℕ) => by simp_rw [natCast_zsmul, smul_assoc]
    | -[n+1] => by simp_rw [negSucc_zsmul, smul_eq_mul, neg_mul, smul_mul_assoc]

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