Library
▹
Algebra
▹
Rings
Definition 2.8.20.
Let
R
be a
ring
,
z
∈
ℤ
,
a
∈
R
. We define:
z
⋅
a
:
=
{
z
⋅
a
if
z
≥
0
(−
z
) ⋅ (−
a
)
if
z
<
0
References.
https://leanprover-community.github.io/mathlib_docs/algebra/group_power/basic.html#gsmul