The integers form a group

This file contains the additive group and multiplicative monoid instances on the integers.

See note [foundational algebra order theory].

Instances

instance Int.instCommMonoid : CommMonoid ℤ

Equations

• Int.instCommMonoid = CommMonoid.mk Int.mul_comm

instance Int.instAddCommGroup : AddCommGroup ℤ

Equations

• Int.instAddCommGroup = AddCommGroup.mk Int.add_comm

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.instAddCommMonoid : AddCommMonoid ℤ

Equations

• Int.instAddCommMonoid = inferInstance

instance Int.instAddMonoid : AddMonoid ℤ

Equations

• Int.instAddMonoid = inferInstance

instance Int.instMonoid : Monoid ℤ

Equations

• Int.instMonoid = inferInstance

instance Int.instCommSemigroup : CommSemigroup ℤ

Equations

• Int.instCommSemigroup = inferInstance

instance Int.instSemigroup : Semigroup ℤ

Equations

• Int.instSemigroup = inferInstance

instance Int.instAddGroup : AddGroup ℤ

Equations

• Int.instAddGroup = inferInstance

instance Int.instAddCommSemigroup : AddCommSemigroup ℤ

Equations

• Int.instAddCommSemigroup = inferInstance

instance Int.instAddSemigroup : AddSemigroup ℤ

Equations

• Int.instAddSemigroup = inferInstance

Miscellaneous lemmas

@[simp]

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

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