The integers are a ring

This file contains the commutative ring instance on ℤ.

See note [foundational algebra order theory].

instance Int.instCommRing : CommRing ℤ

Equations

• One or more equations did not get rendered due to their size.

instance Int.instCancelCommMonoidWithZero : CancelCommMonoidWithZero ℤ

Equations

• Int.instCancelCommMonoidWithZero = { toCommMonoidWithZero := CommSemiring.toCommMonoidWithZero, toIsLeftCancelMulZero := Int.instCancelCommMonoidWithZero._proof_13 }

instance Int.instCharZero : CharZero ℤ

instance Int.instMulDivCancelClass : MulDivCancelClass ℤ

@[simp]

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

theorem Int.cast_mul_eq_zsmul_cast {α : Type u_1} [AddGroupWithOne α] (m n : ℤ) : ↑(m * n) = m • ↑n

Note this holds in marginally more generality than Int.cast_mul

@[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