Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-10 10:05 24aeeaff

View on Github →

feat(data/zmod): integers mod n (#159)

Estimated changes

Modified data/int/basic.lean

added theorem int.coe_nat_ne_zero_iff_pos

added theorem int.coe_nat_nonneg

added theorem int.mod_mod

Modified data/int/modeq.lean

modified theorem int.modeq.coe_nat_modeq_iff

Created data/zmod.lean

added theorem zmod.add_val

added theorem zmod.card_zmod

added theorem zmod.cast_mod_int

added theorem zmod.cast_mod_nat

added theorem zmod.cast_self_eq_zero

added theorem zmod.cast_val

added theorem zmod.eq_iff_modeq_int

added theorem zmod.eq_iff_modeq_nat

added theorem zmod.mk_eq_cast

added theorem zmod.mul_val

added theorem zmod.one_val

added theorem zmod.val_cast_int

added theorem zmod.val_cast_nat

added theorem zmod.val_cast_of_lt

added theorem zmod.zero_val

added def zmod

added theorem zmodp.add_val

added theorem zmodp.cast_mod_int

added theorem zmodp.cast_mod_nat

added theorem zmodp.cast_self_eq_zero:

added theorem zmodp.cast_val

added theorem zmodp.eq_iff_modeq_int

added theorem zmodp.eq_iff_modeq_nat

added theorem zmodp.gcd_a_modeq

added theorem zmodp.mk_eq_cast

added theorem zmodp.mul_inv_eq_gcd

added theorem zmodp.mul_val

added theorem zmodp.one_val

added theorem zmodp.val_cast_int

added theorem zmodp.val_cast_nat

added theorem zmodp.val_cast_of_lt

added theorem zmodp.zero_val

added def zmodp