Mathlib.Algebra.Group.Int.Defs

Module docstring

{"# The integers form a group

This file contains the additive group and multiplicative monoid instances on the integers.

See note [foundational algebra order theory]. ","### Instances ","### Extra instances to short-circuit type class resolution

These also prevent non-computable instances like Int.instNormedCommRing being used to construct these instances non-computably. "}

Int.instCommMonoid instance

: CommMonoid ℤ

Full source

instance instCommMonoid : CommMonoid ℤ where
  mul_comm := Int.mul_comm
  mul_one := Int.mul_one
  one_mul := Int.one_mul
  npow n x := x ^ n
  npow_zero _ := rfl
  npow_succ _ _ := rfl
  mul_assoc := Int.mul_assoc

Commutative Monoid Structure on Integers

Informal description

The integers $\mathbb{Z}$ form a commutative monoid under multiplication.

Int.instAddCommGroup instance

: AddCommGroup ℤ

Full source

instance instAddCommGroup : AddCommGroup ℤ where
  add_comm := Int.add_comm
  add_assoc := Int.add_assoc
  add_zero := Int.add_zero
  zero_add := Int.zero_add
  neg_add_cancel := Int.add_left_neg
  nsmul := (·*·)
  nsmul_zero := Int.zero_mul
  nsmul_succ n x :=
    show (n + 1 : ℤ) * x = n * x + x
    by rw [Int.add_mul, Int.one_mul]
  zsmul := (·*·)
  zsmul_zero' := Int.zero_mul
  zsmul_succ' m n := by
    simp only [Int.natCast_succ, Int.add_mul, Int.add_comm, Int.one_mul]
  zsmul_neg' m n := by simp only [negSucc_eq, Int.natCast_succ, Int.neg_mul]
  sub_eq_add_neg _ _ := Int.sub_eq_add_neg

Additive Commutative Group Structure on Integers

Informal description

The integers $\mathbb{Z}$ form an additive commutative group.

Int.instAddCommMonoid instance

: AddCommMonoid ℤ

Full source

instance instAddCommMonoid    : AddCommMonoid ℤ    := by infer_instance

Additive Commutative Monoid Structure on Integers

Informal description

The integers $\mathbb{Z}$ form an additive commutative monoid.

Int.instAddMonoid instance

: AddMonoid ℤ

Full source

instance instAddMonoid        : AddMonoid ℤ        := by infer_instance

Additive Monoid Structure on Integers

Informal description

The integers $\mathbb{Z}$ form an additive monoid.

Int.instMonoid instance

: Monoid ℤ

Full source

instance instMonoid           : Monoid ℤ           := by infer_instance

Monoid Structure on Integers

Informal description

The integers $\mathbb{Z}$ form a monoid under multiplication.

Int.instCommSemigroup instance

: CommSemigroup ℤ

Full source

instance instCommSemigroup    : CommSemigroup ℤ    := by infer_instance

Commutative Semigroup Structure on Integers

Informal description

The integers $\mathbb{Z}$ form a commutative semigroup under multiplication.

Int.instSemigroup instance

: Semigroup ℤ

Full source

instance instSemigroup        : Semigroup ℤ        := by infer_instance

Semigroup Structure on Integers

Informal description

The integers $\mathbb{Z}$ form a semigroup under multiplication.

Int.instAddGroup instance

: AddGroup ℤ

Full source

instance instAddGroup         : AddGroup ℤ         := by infer_instance

Additive Group Structure on Integers

Informal description

The integers $\mathbb{Z}$ form an additive group.

Int.instAddCommSemigroup instance

: AddCommSemigroup ℤ

Full source

instance instAddCommSemigroup : AddCommSemigroup ℤ := by infer_instance

Additive Commutative Semigroup Structure on Integers

Informal description

The integers $\mathbb{Z}$ form an additive commutative semigroup.

Int.instAddSemigroup instance

: AddSemigroup ℤ

Full source

instance instAddSemigroup     : AddSemigroup ℤ     := by infer_instance

Additive Semigroup Structure on Integers

Informal description

The integers $\mathbb{Z}$ form an additive semigroup.

zsmul_int_int theorem

(a b : ℤ) : a • b = a * b

Full source

lemma zsmul_int_int (a b : ℤ) : a • b = a * b := rfl

Integer Scalar Multiplication Equals Integer Multiplication

Informal description

For any integers $a$ and $b$, the scalar multiplication $a \• b$ is equal to the integer multiplication $a * b$.

zsmul_int_one theorem

(n : ℤ) : n • (1 : ℤ) = n

Full source

lemma zsmul_int_one (n : ℤ) : n • (1 : ℤ) = n := mul_one _

Scalar Multiplication by Identity in Integers: $n \• 1 = n$

Informal description

For any integer $n$, the scalar multiplication of $n$ by the multiplicative identity $1$ is equal to $n$, i.e., $n \• 1 = n$.