Mathlib.Algebra.Ring.Int.Defs

Module docstring

{"# The integers are a ring

This file contains the commutative ring instance on ℤ.

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

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

Int.instCommRing instance

: CommRing ℤ

Full source

instance instCommRing : CommRing ℤ where
  __ := instAddCommGroup
  __ := instCommSemigroup
  zero_mul := Int.zero_mul
  mul_zero := Int.mul_zero
  left_distrib := Int.mul_add
  right_distrib := Int.add_mul
  mul_one := Int.mul_one
  one_mul := Int.one_mul
  npow n x := x ^ n
  npow_zero _ := rfl
  npow_succ _ _ := rfl
  natCast := (·)
  natCast_zero := rfl
  natCast_succ _ := rfl
  intCast := (·)
  intCast_ofNat _ := rfl
  intCast_negSucc _ := rfl

The Commutative Ring Structure on Integers

Informal description

The integers $\mathbb{Z}$ form a commutative ring.

Int.instCancelCommMonoidWithZero instance

: CancelCommMonoidWithZero ℤ

Full source

instance instCancelCommMonoidWithZero : CancelCommMonoidWithZero ℤ where
  mul_left_cancel_of_ne_zero {_a _b _c} ha := (mul_eq_mul_left_iff ha).1

The Cancelative Commutative Monoid with Zero Structure on Integers

Informal description

The integers $\mathbb{Z}$ form a cancelative commutative monoid with zero.

Int.instCharZero instance

: CharZero ℤ

Full source

instance instCharZero : CharZero ℤ where cast_injective _ _ := ofNat.inj

Characteristic Zero Property of Integers

Informal description

The integers $\mathbb{Z}$ have characteristic zero, meaning the canonical map from the natural numbers to $\mathbb{Z}$ is injective.

Int.instMulDivCancelClass instance

: MulDivCancelClass ℤ

Full source

instance instMulDivCancelClass : MulDivCancelClass ℤ where mul_div_cancel _ _ := mul_ediv_cancel _

Multiplication-Division Cancellation Property for Integers

Informal description

The integers $\mathbb{Z}$ satisfy the multiplication-division cancellation property, meaning that for any integers $a, b \in \mathbb{Z}$ with $b \neq 0$, we have $a \cdot b / b = a$ and $a \cdot b / a = b$ when $a \neq 0$.

Int.cast_mul theorem

{α : Type*} [NonAssocRing α] : ∀ m n, ((m * n : ℤ) : α) = m * n

Full source

@[simp, norm_cast]
lemma cast_mul {α : Type*} [NonAssocRing α] : ∀ m n, ((m * n : ℤ) : α) = m * n := fun m => by
  obtain ⟨m, rfl | rfl⟩ := Int.eq_nat_or_neg m
  · induction m with
    | zero => simp
    | succ m ih => simp_all [add_mul]
  · induction m with
    | zero => simp
    | succ m ih => simp_all [add_mul]

Canonical Homomorphism Preserves Integer Multiplication: $\text{cast}(m \cdot n) = \text{cast}(m) \cdot \text{cast}(n)$

Informal description

For any non-associative ring $\alpha$ and any integers $m$ and $n$, the canonical homomorphism from the integers to $\alpha$ preserves multiplication, i.e., $(m \cdot n : \mathbb{Z}) : \alpha = m \cdot n$.

Int.cast_mul_eq_zsmul_cast theorem

{α : Type*} [AddGroupWithOne α] : ∀ m n : ℤ, ↑(m * n) = m • (n : α)

Full source

/-- Note this holds in marginally more generality than `Int.cast_mul` -/
lemma cast_mul_eq_zsmul_cast {α : Type*} [AddGroupWithOne α] :
    ∀ m n : ℤ, ↑(m * n) = m • (n : α) :=
  fun m ↦ Int.induction_on m (by simp) (fun _ ih ↦ by simp [add_mul, add_zsmul, ih]) fun _ ih ↦ by
    simp only [sub_mul, one_mul, cast_sub, ih, sub_zsmul, one_zsmul, ← sub_eq_add_neg, forall_const]

Integer Multiplication Cast as Scalar Multiplication: $\text{cast}(m \cdot n) = m \cdot \text{cast}(n)$

Informal description

For any additive group with one $\alpha$ and any integers $m$ and $n$, the canonical homomorphism from the integers to $\alpha$ satisfies $\text{cast}(m \cdot n) = m \cdot \text{cast}(n)$, where the right-hand side uses integer scalar multiplication.

Int.cast_pow theorem

{R : Type*} [Ring R] (n : ℤ) (m : ℕ) : ↑(n ^ m) = (n ^ m : R)

Full source

@[simp, norm_cast] lemma cast_pow {R : Type*} [Ring R] (n : ℤ) (m : ℕ) :
    ↑(n ^ m) = (n ^ m : R) := by
  induction m <;> simp [_root_.pow_succ, *]

Canonical Homomorphism Preserves Integer Exponentiation: $\text{cast}(n^m) = n^m$

Informal description

For any ring $R$ and any integer $n$, the canonical homomorphism from the integers to $R$ preserves exponentiation, i.e., for any natural number $m$, we have $(n^m : \mathbb{Z}) : R = n^m$.

Int.instCommSemiring instance

: CommSemiring ℤ

Full source

instance instCommSemiring : CommSemiring ℤ := inferInstance

The Commutative Semiring Structure on Integers

Informal description

The integers $\mathbb{Z}$ form a commutative semiring.

Int.instSemiring instance

: Semiring ℤ

Full source

instance instSemiring     : Semiring ℤ     := inferInstance

The Semiring Structure on Integers

Informal description

The integers $\mathbb{Z}$ form a semiring.

Int.instRing instance

: Ring ℤ

Full source

instance instRing         : Ring ℤ         := inferInstance

The Ring Structure on Integers

Informal description

The integers $\mathbb{Z}$ form a ring.

Int.instDistrib instance

: Distrib ℤ

Full source

instance instDistrib      : Distrib ℤ      := inferInstance

Distributive Structure on Integers

Informal description

The integers $\mathbb{Z}$ are equipped with a distributive structure where multiplication distributes over addition.