The integers are a ring

This file contains the commutative ring instance on ℤ.

See note [foundational algebra order theory].

instance Int.instCommRing : CommRing ℤ

Equations

• Int.instCommRing = let __spread.0 := Int.instAddCommGroup; let __spread.1 := Int.instCommSemigroup; CommRing.mk ⋯

instance Int.instMulDivCancelClass : MulDivCancelClass ℤ

Equations

• Int.instMulDivCancelClass = ⋯

@[simp]

theorem Int.cast_mul {α : Type u_1} [NonAssocRing α] (m : ℤ) (n : ℤ) : ↑(m * n) = ↑m * ↑n

@[simp]

theorem Int.cast_pow {R : Type u_1} [Ring R] (n : ℤ) (m : ℕ) : ↑(n ^ m) = ↑n ^ m

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.

instance Int.instCommSemiring : CommSemiring ℤ

Equations

• Int.instCommSemiring = inferInstance

instance Int.instSemiring : Semiring ℤ

Equations

• Int.instSemiring = inferInstance

instance Int.instRing : Ring ℤ

Equations

• Int.instRing = inferInstance

instance Int.instDistrib : Distrib ℤ

Equations

• Int.instDistrib = inferInstance

instance Int.instCharZero : CharZero ℤ

Equations

• Int.instCharZero = ⋯