Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-08 01:00 2bd5e215

View on Github →

feat(data/int/modeq): Modular arithmetic for integers

Estimated changes

Created data/int/modeq.lean

added theorem int.modeq.coe_nat_modeq_iff

added theorem int.modeq.modeq_add

added theorem int.modeq.modeq_add_cancel_left

added theorem int.modeq.modeq_add_cancel_right

added theorem int.modeq.modeq_iff_dvd

added theorem int.modeq.modeq_mul

added theorem int.modeq.modeq_mul_left'

added theorem int.modeq.modeq_mul_left

added theorem int.modeq.modeq_mul_right'

added theorem int.modeq.modeq_mul_right

added theorem int.modeq.modeq_neg

added theorem int.modeq.modeq_of_dvd_of_modeq

added theorem int.modeq.modeq_sub

added theorem int.modeq.modeq_zero_iff

added def int.modeq