English
Equality of scalar actions under natural-number cast: for all n ∈ ℕ and b ∈ M, (n : R) • b = n • b.
Русский
Согласование действия скаляра при копировании через естественное включение: для всех n ∈ ℕ и b ∈ M, (n : R) • b = n • b.
LaTeX
$$$\forall n \in \mathbb{N},\; (n:\,R)\,\cdot\, b = n\cdot b$$$
Lean4
/-- An `AddCommMonoid` that is a `Module` over a `Ring` carries a natural `AddCommGroup`
structure.
See note [reducible non-instances]. -/
abbrev addCommMonoidToAddCommGroup [Ring R] [AddCommMonoid M] [Module R M] : AddCommGroup M :=
{ (inferInstance : AddCommMonoid M) with
neg := fun a => (-1 : R) • a
neg_add_cancel := fun a =>
show (-1 : R) • a + a = 0 by
nth_rw 2 [← one_smul R a]
rw [← add_smul, neg_add_cancel, zero_smul]
zsmul := fun z a => (z : R) • a
zsmul_zero' := fun a => by simpa only [Int.cast_zero] using zero_smul R a
zsmul_succ' := fun z a => by simp [add_comm, add_smul]
zsmul_neg' := fun z a => by simp [← smul_assoc] }
