Commit 2023-03-18 17:27 98f36162

View on Github →

feat: port Data.ZMod.Basic (#2870)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/ZMod/Basic.lean

added theorem Nat.le_div_two_iff_mul_two_le

added theorem Prod.fst_zmod_cast

added theorem Prod.snd_zmod_cast

added theorem RingHom.ext_zmod

added theorem ZMod.addOrderOf_coe'

added theorem ZMod.addOrderOf_coe

added theorem ZMod.addOrderOf_one

added def ZMod.cast

added def ZMod.castHom

added theorem ZMod.castHom_apply

added theorem ZMod.castHom_bijective

added theorem ZMod.castHom_injective

added theorem ZMod.cast_add'

added theorem ZMod.cast_add

added theorem ZMod.cast_eq_val

added theorem ZMod.cast_id'

added theorem ZMod.cast_id

added theorem ZMod.cast_int_cast'

added theorem ZMod.cast_int_cast

added theorem ZMod.cast_mul'

added theorem ZMod.cast_mul

added theorem ZMod.cast_nat_cast'

added theorem ZMod.cast_nat_cast

added theorem ZMod.cast_neg

added theorem ZMod.cast_neg_one

added theorem ZMod.cast_one'

added theorem ZMod.cast_one

added theorem ZMod.cast_pow'

added theorem ZMod.cast_pow

added theorem ZMod.cast_sub'

added theorem ZMod.cast_sub

added theorem ZMod.cast_sub_one

added theorem ZMod.cast_zero

added def ZMod.chineseRemainder

added theorem ZMod.coe_add_eq_ite

added theorem ZMod.coe_int_cast

added theorem ZMod.coe_mul_inv_eq_one

added theorem ZMod.coe_unitOfCoprime

added theorem ZMod.coe_valMinAbs

added theorem ZMod.eq_iff_modEq_nat

added theorem ZMod.injective_valMinAbs

added theorem ZMod.int_cast_cast

added theorem ZMod.int_cast_comp_cast

added theorem ZMod.int_cast_eq_int_cast_iff'

added theorem ZMod.int_cast_eq_int_cast_iff

added theorem ZMod.int_cast_eq_int_cast_iff_dvd_sub

added theorem ZMod.int_cast_mod

added theorem ZMod.int_cast_rightInverse

added theorem ZMod.int_cast_surjective

added theorem ZMod.int_cast_zmod_cast

added theorem ZMod.int_cast_zmod_eq_zero_iff_dvd

added theorem ZMod.int_coe_zmod_eq_iff

added def ZMod.inv

added theorem ZMod.inv_coe_unit

added theorem ZMod.inv_mul_of_unit

added theorem ZMod.inv_zero

added theorem ZMod.ker_int_castAddHom

added theorem ZMod.ker_int_castRingHom

added theorem ZMod.le_div_two_iff_lt_neg

added def ZMod.lift

added theorem ZMod.lift_castAddHom

added theorem ZMod.lift_coe

added theorem ZMod.lift_comp_castAddHom

added theorem ZMod.lift_comp_coe

added theorem ZMod.mul_inv_eq_gcd

added theorem ZMod.mul_inv_of_unit

added theorem ZMod.natAbs_min_of_le_div_two

added theorem ZMod.natAbs_mod_two

added theorem ZMod.natAbs_valMinAbs_add_le

added theorem ZMod.natAbs_valMinAbs_le

added theorem ZMod.natAbs_valMinAbs_neg

added theorem ZMod.nat_cast_comp_val

added theorem ZMod.nat_cast_eq_nat_cast_iff'

added theorem ZMod.nat_cast_eq_nat_cast_iff

added theorem ZMod.nat_cast_mod

added theorem ZMod.nat_cast_natAbs_valMinAbs

added theorem ZMod.nat_cast_rightInverse

added theorem ZMod.nat_cast_self'

added theorem ZMod.nat_cast_self

added theorem ZMod.nat_cast_toNat

added theorem ZMod.nat_cast_val

added theorem ZMod.nat_cast_zmod_eq_zero_iff_dvd

added theorem ZMod.nat_cast_zmod_surjective

added theorem ZMod.nat_cast_zmod_val

added theorem ZMod.nat_coe_zmod_eq_iff

added theorem ZMod.ne_neg_self

added theorem ZMod.neg_eq_self_iff

added theorem ZMod.neg_eq_self_mod_two

added theorem ZMod.neg_one_ne_one

added theorem ZMod.neg_val'

added theorem ZMod.neg_val

added theorem ZMod.prime_ne_zero

added theorem ZMod.ringChar_zmod_n

added def ZMod.ringEquivCongr

added theorem ZMod.ringHom_eq_of_ker_eq

added theorem ZMod.ringHom_map_cast

added theorem ZMod.ringHom_rightInverse

added theorem ZMod.ringHom_surjective

added def ZMod.unitOfCoprime

added def ZMod.unitsEquivCoprime

added def ZMod.val

added def ZMod.valMinAbs

added theorem ZMod.valMinAbs_def_pos

added theorem ZMod.valMinAbs_def_zero

added theorem ZMod.valMinAbs_eq_zero

added theorem ZMod.valMinAbs_mem_Ioc

added theorem ZMod.valMinAbs_mul_two_eq_iff

added theorem ZMod.valMinAbs_natAbs_eq_min

added theorem ZMod.valMinAbs_neg_of_ne_half

added theorem ZMod.valMinAbs_nonneg_iff

added theorem ZMod.valMinAbs_spec

added theorem ZMod.valMinAbs_zero

added theorem ZMod.val_add

added theorem ZMod.val_cast_of_lt

added theorem ZMod.val_coe_unit_coprime

added theorem ZMod.val_eq_ite_valMinAbs

added theorem ZMod.val_eq_zero

added theorem ZMod.val_injective

added theorem ZMod.val_int_cast

added theorem ZMod.val_le

added theorem ZMod.val_lt

added theorem ZMod.val_mul'

added theorem ZMod.val_mul

added theorem ZMod.val_nat_cast

added theorem ZMod.val_neg'

added theorem ZMod.val_neg_one

added theorem ZMod.val_one'

added theorem ZMod.val_one

added theorem ZMod.val_one_eq_one_mod

added theorem ZMod.val_zero