Basic algebraic instances on the integers

This file contains instances on ℤ. The stronger one is Int.linearOrderedCommRing.

instance Int.instCommRingInt : CommRing ℤ

Equations

• Int.instCommRingInt = CommRing.mk Int.mul_comm

@[simp]

theorem Int.cast_id {n : ℤ} : ↑n = n

@[simp]

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

theorem Int.cast_Nat_cast {n : ℕ} {R : Type u_1} [AddGroupWithOne R] : ↑↑n = ↑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.instAddCommMonoidInt : AddCommMonoid ℤ

Equations

• Int.instAddCommMonoidInt = inferInstance

instance Int.instAddMonoidInt : AddMonoid ℤ

Equations

• Int.instAddMonoidInt = inferInstance

instance Int.instMonoidInt : Monoid ℤ

Equations

• Int.instMonoidInt = inferInstance

instance Int.instCommMonoidInt : CommMonoid ℤ

Equations

• Int.instCommMonoidInt = inferInstance

instance Int.instCommSemigroupInt : CommSemigroup ℤ

Equations

• Int.instCommSemigroupInt = inferInstance

instance Int.instSemigroupInt : Semigroup ℤ

Equations

• Int.instSemigroupInt = inferInstance

instance Int.instAddCommGroupInt : AddCommGroup ℤ

Equations

• Int.instAddCommGroupInt = inferInstance

instance Int.instAddGroupInt : AddGroup ℤ

Equations

• Int.instAddGroupInt = inferInstance

instance Int.instAddCommSemigroupInt : AddCommSemigroup ℤ

Equations

• Int.instAddCommSemigroupInt = inferInstance

instance Int.instAddSemigroupInt : AddSemigroup ℤ

Equations

• Int.instAddSemigroupInt = inferInstance

instance Int.instCommSemiringInt : CommSemiring ℤ

Equations

• Int.instCommSemiringInt = inferInstance

instance Int.instSemiringInt : Semiring ℤ

Equations

• Int.instSemiringInt = inferInstance

instance Int.instRingInt : Ring ℤ

Equations

• Int.instRingInt = inferInstance

instance Int.instDistribInt : Distrib ℤ

Equations

• Int.instDistribInt = inferInstance

theorem Int.natAbs_pow (n : ℤ) (k : ℕ) : Int.natAbs (n ^ k) = Int.natAbs n ^ k

theorem Int.coe_nat_strictMono : StrictMono fun (x : ℕ) => ↑x

theorem Int.toAdd_pow (a : Multiplicative ℤ) (b : ℕ) : Multiplicative.toAdd (a ^ b) = Multiplicative.toAdd a * ↑b

theorem Int.toAdd_zpow (a : Multiplicative ℤ) (b : ℤ) : Multiplicative.toAdd (a ^ b) = Multiplicative.toAdd a * b

@[simp]

theorem Int.ofAdd_mul (a : ℤ) (b : ℤ) : Multiplicative.ofAdd (a * b) = Multiplicative.ofAdd a ^ b

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

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