Documentation

Mathlib.Data.Int.Basic

Basic algebraic instances on the integers #

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

@[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 {R : Type u_1} {n : } [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.

Equations
Equations
Equations
theorem Int.natAbs_pow (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