The integers are a ring

This file contains the commutative ring instance on ℤ.

See note [foundational algebra order theory].

@[implicit_reducible]

instance Int.instCommRing : CommRing ℤ

Equations

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

instance Int.instIsCancelMulZero : IsCancelMulZero ℤ

instance Int.instIsDomain : IsDomain ℤ

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.

@[implicit_reducible]

instance Int.instCommSemiring : CommSemiring ℤ

Equations

• Int.instCommSemiring = inferInstance

@[implicit_reducible]

instance Int.instSemiring : Semiring ℤ

Equations

• Int.instSemiring = inferInstance

@[implicit_reducible]

instance Int.instRing : Ring ℤ

Equations

• Int.instRing = inferInstance

@[implicit_reducible]

instance Int.instDistrib : Distrib ℤ

Equations

• Int.instDistrib = inferInstance